equal
deleted
inserted
replaced
642 apply(erule_tac c="t2a" in Abs_lst1_fcb2') |
642 apply(erule_tac c="t2a" in Abs_lst1_fcb2') |
643 apply (erule fresh_eqvt_at) |
643 apply (erule fresh_eqvt_at) |
644 apply (simp add: finite_supp) |
644 apply (simp add: finite_supp) |
645 apply (simp add: fresh_Inl var_fresh_subst) |
645 apply (simp add: fresh_Inl var_fresh_subst) |
646 apply(simp add: fresh_star_def) |
646 apply(simp add: fresh_star_def) |
647 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst_eqvt) |
647 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst.eqvt) |
648 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst_eqvt) |
648 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst.eqvt) |
649 done |
649 done |
650 |
650 |
651 |
651 |
652 (* a small test |
652 (* a small test |
653 termination (eqvt) sorry |
653 termination (eqvt) sorry |