equal
deleted
inserted
replaced
95 apply(rule at_set_avoiding2) |
95 apply(rule at_set_avoiding2) |
96 apply(simp add: finite_supp) |
96 apply(simp add: finite_supp) |
97 apply(simp add: finite_supp) |
97 apply(simp add: finite_supp) |
98 apply(simp add: finite_supp) |
98 apply(simp add: finite_supp) |
99 apply(simp add: trm_assn.fresh fresh_star_def) |
99 apply(simp add: trm_assn.fresh fresh_star_def) |
100 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assn))) \<sharp>* (c::'a::fs) \<and> supp ([bn assn]lst.trm) \<sharp>* q") |
100 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assn))) \<sharp>* (c::'a::fs, fv_bn assn) \<and> supp ([bn assn]lst.trm) \<sharp>* q") |
101 apply(erule exE) |
101 apply(erule exE) |
102 apply(erule conjE) |
102 apply(erule conjE) |
|
103 apply(simp add: set_eqvt) |
|
104 apply(subst (asm) tt) |
103 apply(rule_tac assms(4)) |
105 apply(rule_tac assms(4)) |
104 apply(simp add: set_eqvt) |
106 apply(simp add: fresh_star_prod) |
105 apply(simp add: tt) |
107 apply(erule conjE) |
|
108 apply(assumption) |
106 apply(simp) |
109 apply(simp) |
107 apply(simp add: trm_assn.eq_iff) |
110 apply(simp add: trm_assn.eq_iff) |
108 apply(drule supp_perm_eq[symmetric]) |
111 apply(drule supp_perm_eq[symmetric]) |
109 apply(simp) |
112 apply(simp) |
110 apply(simp add: tt uu) |
113 apply(simp add: tt uu) |