278 apply (case_tac x) |
278 apply (case_tac x) |
279 apply (rule_tac y="c" and c="(a,b)" in trm_assn.strong_exhaust(1)) |
279 apply (rule_tac y="c" and c="(a,b)" in trm_assn.strong_exhaust(1)) |
280 apply (auto simp add: fresh_star_def)[3] |
280 apply (auto simp add: fresh_star_def)[3] |
281 apply (drule_tac x="assn" in meta_spec) |
281 apply (drule_tac x="assn" in meta_spec) |
282 apply (simp add: Abs1_eq_iff alpha_bn_refl) |
282 apply (simp add: Abs1_eq_iff alpha_bn_refl) |
283 apply auto |
283 apply simp_all[7] |
|
284 prefer 2 |
|
285 apply(simp) |
|
286 apply(simp) |
|
287 apply(erule conjE)+ |
284 apply (erule_tac c="(sa, ta)" in Abs_lst1_fcb2) |
288 apply (erule_tac c="(sa, ta)" in Abs_lst1_fcb2) |
285 apply (simp add: Abs_fresh_iff) |
289 apply (simp add: Abs_fresh_iff) |
286 apply (simp add: fresh_star_def) |
290 apply (simp add: fresh_star_def) |
287 apply (simp_all add: fresh_star_Pair_elim perm_supp_eq eqvt_at_def)[2] |
291 apply (simp_all add: fresh_star_Pair_elim perm_supp_eq eqvt_at_def)[2] |
288 apply (simp add: bn_apply_assn2) |
292 apply (simp add: bn_apply_assn2) |
|
293 apply(erule conjE)+ |
|
294 apply(rule conjI) |
289 apply (erule_tac c="(sa, ta)" in Abs_lst_fcb2) |
295 apply (erule_tac c="(sa, ta)" in Abs_lst_fcb2) |
290 apply (simp add: fresh_star_def Abs_fresh_iff) |
296 apply (simp add: fresh_star_def Abs_fresh_iff) |
291 apply assumption+ |
297 apply assumption+ |
292 apply (simp_all add: fresh_star_Pair_elim perm_supp_eq eqvt_at_def trm_assn.fv_bn_eqvt)[2] |
298 apply (simp_all add: fresh_star_Pair_elim perm_supp_eq eqvt_at_def trm_assn.fv_bn_eqvt)[2] |
293 apply (erule alpha_bn_inducts) |
299 apply (erule alpha_bn_inducts) |