--- a/Quot/Nominal/LamEx2.thy	Tue Feb 02 10:43:48 2010 +0100
+++ b/Quot/Nominal/LamEx2.thy	Tue Feb 02 11:23:17 2010 +0100
@@ -122,6 +122,23 @@
 apply(auto)
 done
 
+lemma alpha_gen_eqvt_atom:
+  assumes a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"
+  shows "\<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) \<Longrightarrow> \<exists>pia. ({atom (pi \<bullet> a)}, pi \<bullet> t) \<approx>gen R f pia ({atom (pi \<bullet> b)}, pi \<bullet> s)"
+apply(erule exE)
+apply(rule_tac x="pi \<bullet> pia" in exI)
+apply(simp add: alpha_gen.simps)
+apply(erule conjE)+
+apply(rule conjI)+
+apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
+apply(simp add: a[symmetric] atom_eqvt eqvts)
+apply(rule conjI)
+apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
+apply(simp add: a[symmetric] eqvts atom_eqvt)
+apply(subst permute_eqvt[symmetric])
+apply(simp)
+done
+
 text {* should be automatic with new version of eqvt-machinery *}
 lemma alpha_eqvt:
   shows "t \<approx> s \<Longrightarrow> (pi \<bullet> t) \<approx> (pi \<bullet> s)"
@@ -130,18 +147,9 @@
 apply(simp add: a2)
 apply(simp)
 apply(rule a3)
-apply(erule exE)
-apply(rule_tac x="pi \<bullet> pia" in exI)
-apply(simp add: alpha_gen.simps)
-apply(erule conjE)+
-apply(rule conjI)+
-apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
-apply(simp add: eqvts atom_eqvt)
-apply(rule conjI)
-apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
-apply(simp add: eqvts atom_eqvt)
-apply(subst permute_eqvt[symmetric])
-apply(simp)
+apply(rule alpha_gen_eqvt_atom)
+apply(rule rfv_eqvt)
+apply assumption
 done
 
 lemma alpha_refl: