equal
deleted
inserted
replaced
106 apply (simp add: eqvts eqvts_raw) |
106 apply (simp add: eqvts eqvts_raw) |
107 apply (rule at_set_avoiding2) |
107 apply (rule at_set_avoiding2) |
108 apply (simp add: fin_fset_to_set) |
108 apply (simp add: fin_fset_to_set) |
109 apply (simp add: finite_supp) |
109 apply (simp add: finite_supp) |
110 apply (simp add: eqvts finite_supp) |
110 apply (simp add: eqvts finite_supp) |
111 apply (subst atom_eqvt_raw[symmetric]) |
111 apply (rule_tac p=" -p" in permute_boolE) |
112 apply (subst fmap_eqvt[symmetric]) |
112 apply(simp add: eqvts) |
113 apply (subst fset_to_set_eqvt[symmetric]) |
113 apply(simp add: permute_fun_def atom_eqvt) |
114 apply (simp only: fresh_star_permute_iff) |
|
115 apply (simp add: fresh_star_def) |
114 apply (simp add: fresh_star_def) |
116 apply clarify |
115 apply clarify |
117 apply (simp add: fresh_def) |
116 apply (simp add: fresh_def) |
118 apply (simp add: ty_tys_supp) |
117 apply (simp add: ty_tys_supp) |
119 done |
118 done |