380 lemma alpha_abs_set_stronger1:

   381   fixes x::"'a::fs"

   382   assumes  fin: "finite as"

   383   and     asm: "(as, x) \<approx>set (op =) supp p' (as', x')"

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

   385 proof -

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

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

   388     by (simp add: atom_set_perm_eq)

   389   have za: "finite ((supp x) \<union> as)" using fin by (simp add: finite_supp)

   390   obtain p where *: "\<forall>b \<in> ((supp x) \<union> as). p \<bullet> b = p' \<bullet> b" and **: "supp p \<subseteq> ((supp x) \<union> as) \<union> p' \<bullet> ((supp x) \<union> as)"

   391     using set_renaming_perm[OF za] by blast

   392   from * have "\<forall>b \<in> supp x. p \<bullet> b = p' \<bullet> b" by blast

   393   then have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto

   394   from * have "\<forall>b \<in> as. p \<bullet> b = p' \<bullet> b" by blast

   395   then have zb: "p \<bullet> as = p' \<bullet> as" using supp_perm_perm_eq by (metis fin supp_finite_atom_set)

   396   have zc: "p' \<bullet> as = as'" using asm by (simp add: alphas)

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

   398     by (auto simp add: fresh_star_def fresh_perm)

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

   400     by (auto simp add: fresh_star_def fresh_def)

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

   402   have "supp p \<subseteq> supp x \<union> as \<union> p' \<bullet> supp x \<union> p' \<bullet> as" using ** using union_eqvt by blast

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

   404     using b by simp

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

   406     by (simp add: union_eqvt)

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

   408     using # by auto

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

   410     by auto

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

   412     by (metis Int_commute Un_commute sup_inf_absorb)

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

   414     by blast

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

   416   then have "supp p \<subseteq> as \<union> p' \<bullet> as" using 2 by blast

   417   moreover 

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

   419   ultimately 

   420   show "\<exists>p. (as, x) \<approx>set (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as'" using zc by blast

   421 qed

   422