61 | "Cbinders (Type2 t T) = {atom t}"

    61 | "Cbinders (Type2 t T) = {atom t}"

    62 | "Cbinders (SStru x S) = {atom x}"

    62 | "Cbinders (SStru x S) = {atom x}"

    63 | "Cbinders (SVal v T) = {atom v}"

    63 | "Cbinders (SVal v T) = {atom v}"

    64 

    64 

    65 

    65 

    66 thm modules.distinct

    70 thm modules.distinct

    67 thm modules.induct

    71 thm modules.induct

    68 thm modules.exhaust

    72 thm modules.exhaust

    69 thm modules.fv_defs

    73 thm modules.fv_defs

    70 thm modules.bn_defs

    74 thm modules.bn_defs