345 lemma alpha_abs_res_stronger1:

   346   fixes x::"'a::fs"

   347   assumes asm: "(as, x) \<approx>res (op =) supp p' (as', x')" 

   348   shows "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> (supp x \<inter> as) \<union> (supp x' \<inter> as')" 

   349 proof -

   350   from asm have 0: "(supp x - as) \<sharp>* p'" by  (auto simp only: alphas)

   351   then have #: "p' \<bullet> (supp x - as) = (supp x - as)" 

   352     by (simp add: atom_set_perm_eq)

   353   have "finite (supp x)" by (simp add: finite_supp)

   354   then obtain p where *: "\<forall>b \<in> supp x. p \<bullet> b = p' \<bullet> b" and **: "supp p \<subseteq> supp x \<union> p' \<bullet> supp x"

   355     using set_renaming_perm by blast

   356   from * have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto

   357   from 0 have 1: "(supp x - as) \<sharp>* p" using *

   358     by (auto simp add: fresh_star_def fresh_perm)

   359   then have 2: "(supp x - as) \<inter> supp p = {}"

   360     by (auto simp add: fresh_star_def fresh_def)

   361   have b: "supp x = (supp x - as) \<union> (supp x \<inter> as)" by auto

   362   have "supp p \<subseteq> supp x \<union> p' \<bullet> supp x" using ** by simp

   363   also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> (p' \<bullet> ((supp x - as) \<union> (supp x \<inter> as)))" 

   364     using b by simp

   365   also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> ((p' \<bullet> (supp x - as)) \<union> (p' \<bullet> (supp x \<inter> as)))"

   366     by (simp add: union_eqvt)

   367   also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> (p' \<bullet> (supp x \<inter> as))" 

   368     using # by auto

   369   also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> (supp x' \<inter> as')" using asm

   370     by (simp add: supp_property_res)

   371   finally have "supp p \<subseteq> (supp x - as) \<union> (supp x \<inter> as) \<union> (supp x' \<inter> as')" .

   372   then 

   373   have "supp p \<subseteq> (supp x \<inter> as) \<union> (supp x' \<inter> as')" using 2 by auto

   374   moreover 

   375   have "(as, x) \<approx>res (op =) supp p (as', x')" using asm 1 a by (simp add: alphas)

   376   ultimately 

   377   show "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> (supp x \<inter> as) \<union> (supp x' \<inter> as')" by blast

   378 qed

   379