31 thm trm_lts.distinct

    31 thm trm_lts.distinct

    32 thm trm_lts.supp

    32 thm trm_lts.supp

    33 thm trm_lts.fv[simplified trm_lts.supp]

    33 thm trm_lts.fv[simplified trm_lts.supp]

    34 

    34 

    35 declare permute_trm_raw_permute_lts_raw.simps[eqvt]

    35 declare permute_trm_raw_permute_lts_raw.simps[eqvt]

    37 

    36 

    38 equivariance alpha_trm_raw

    37 equivariance alpha_trm_raw

    39 

    38 

    40 (* why is this not in HOL simpset? *)

    39 (* why is this not in HOL simpset? *)

    41 lemma set_sub: "{a, b} - {b} = {a} - {b}"

    40 lemma set_sub: "{a, b} - {b} = {a} - {b}"