28   apply(simp add: fresh_star_def fresh_Pair)

    28   apply(simp add: fresh_star_def fresh_Pair)

    29   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)

    29   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)

    30   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)

    30   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)

    31   done

    31   done

    32 

    32 

    34   by lexicographic_order

    34   by lexicographic_order

    35 

    35 

    36 lemma forget:

    36 lemma forget:

    37   shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"

    37   shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"

    38   by (nominal_induct t avoiding: x s rule: lam.strong_induct)

    38   by (nominal_induct t avoiding: x s rule: lam.strong_induct)