equal
deleted
inserted
replaced
263 apply (simp add: fresh_star_def fresh_def) |
263 apply (simp add: fresh_star_def fresh_def) |
264 apply (simp (no_asm) only: supp_eqvt[symmetric] Pair_eqvt[symmetric]) |
264 apply (simp (no_asm) only: supp_eqvt[symmetric] Pair_eqvt[symmetric]) |
265 apply (subgoal_tac "p \<bullet> supp (subst \<theta>' T) \<subseteq> p \<bullet> supp (\<theta>', T)") |
265 apply (subgoal_tac "p \<bullet> supp (subst \<theta>' T) \<subseteq> p \<bullet> supp (\<theta>', T)") |
266 apply (erule subsetD) |
266 apply (erule subsetD) |
267 apply (simp add: supp_eqvt) |
267 apply (simp add: supp_eqvt) |
268 apply (metis le_eqvt permute_boolI) |
268 apply (metis permute_pure subset_eqvt) |
269 apply (rule perm_supp_eq) |
269 apply (rule perm_supp_eq) |
270 apply (simp add: fresh_def fresh_star_def) |
270 apply (simp add: fresh_def fresh_star_def) |
271 apply blast |
271 apply blast |
272 done |
272 done |
273 |
273 |
305 apply(clarify) |
305 apply(clarify) |
306 apply(simp add: alphas fresh_star_def ty_tys.supp supp_at_base) |
306 apply(simp add: alphas fresh_star_def ty_tys.supp supp_at_base) |
307 apply auto |
307 apply auto |
308 done |
308 done |
309 |
309 |
310 |
|
311 |
|
312 |
|
313 end |
310 end |