--- a/Nominal/Abs.thy	Thu Feb 25 07:48:33 2010 +0100
+++ b/Nominal/Abs.thy	Thu Feb 25 07:48:57 2010 +0100
@@ -113,11 +113,12 @@
   apply(simp)
   done
 
-lemma alpha_gen_atom_eqvt:
-  assumes a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"
-  and     b: "\<exists>pia. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia ({atom b}, s)"
-  shows  "\<exists>pia. ({atom (pi \<bullet> a)}, pi \<bullet> t) \<approx>gen R f pia ({atom (pi \<bullet> b)}, pi \<bullet> s)"
-  using b 
+lemma alpha_gen_compose_eqvt:
+  assumes b: "\<exists>pia. (g d, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia (g e, s)"
+  and     c: "\<And>y. pi \<bullet> (g y) = g (pi \<bullet> y)"
+  and     a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"
+  shows  "\<exists>pia. (g (pi \<bullet> d), pi \<bullet> t) \<approx>gen R f pia (g (pi \<bullet> e), pi \<bullet> s)"
+  using b
   apply -
   apply(erule exE)
   apply(rule_tac x="pi \<bullet> pia" in exI)
@@ -125,10 +126,10 @@
   apply(erule conjE)+
   apply(rule conjI)
   apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
-  apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt)
+  apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric])
   apply(rule conjI)
   apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
-  apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt)
+  apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric])
   apply(subst permute_eqvt[symmetric])
   apply(simp)
   done