--- a/Nominal/Nominal2_Abs.thy	Tue Jan 18 06:55:18 2011 +0100
+++ b/Nominal/Nominal2_Abs.thy	Tue Jan 18 11:02:57 2011 +0100
@@ -342,6 +342,41 @@
     by (auto dest: disjoint_right_eq)
 qed
 
+lemma alpha_abs_res_stronger1:
+  fixes x::"'a::fs"
+  assumes asm: "(as, x) \<approx>res (op =) supp p' (as', x')" 
+  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')" 
+proof -
+  from asm have 0: "(supp x - as) \<sharp>* p'" by  (auto simp only: alphas)
+  then have #: "p' \<bullet> (supp x - as) = (supp x - as)" 
+    by (simp add: atom_set_perm_eq)
+  have "finite (supp x)" by (simp add: finite_supp)
+  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"
+    using set_renaming_perm by blast
+  from * have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto
+  from 0 have 1: "(supp x - as) \<sharp>* p" using *
+    by (auto simp add: fresh_star_def fresh_perm)
+  then have 2: "(supp x - as) \<inter> supp p = {}"
+    by (auto simp add: fresh_star_def fresh_def)
+  have b: "supp x = (supp x - as) \<union> (supp x \<inter> as)" by auto
+  have "supp p \<subseteq> supp x \<union> p' \<bullet> supp x" using ** by simp
+  also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> (p' \<bullet> ((supp x - as) \<union> (supp x \<inter> as)))" 
+    using b by simp
+  also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> ((p' \<bullet> (supp x - as)) \<union> (p' \<bullet> (supp x \<inter> as)))"
+    by (simp add: union_eqvt)
+  also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> (p' \<bullet> (supp x \<inter> as))" 
+    using # by auto
+  also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> (supp x' \<inter> as')" using asm
+    by (simp add: supp_property_res)
+  finally have "supp p \<subseteq> (supp x - as) \<union> (supp x \<inter> as) \<union> (supp x' \<inter> as')" .
+  then 
+  have "supp p \<subseteq> (supp x \<inter> as) \<union> (supp x' \<inter> as')" using 2 by auto
+  moreover 
+  have "(as, x) \<approx>res (op =) supp p (as', x')" using asm 1 a by (simp add: alphas)
+  ultimately 
+  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
+qed
+
 
 
 section {* Quotient types *}