--- a/Quot/Nominal/Terms.thy	Mon Feb 22 12:12:32 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Mon Feb 22 13:41:13 2010 +0100
@@ -116,6 +116,23 @@
   apply(simp add: permute_eqvt[symmetric])
   done
 
+lemma alpha_gen_atom_sym:
+  assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
+  shows "\<exists>pi. (aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s) \<Longrightarrow>
+        \<exists>pi. (ab, s) \<approx>gen R f pi (aa, t)"
+  apply(erule exE)
+  apply(rule_tac x="- pi" in exI)
+  apply(simp add: alpha_gen.simps)
+  apply(erule conjE)+
+  apply(rule conjI)
+  apply(simp add: fresh_star_def fresh_minus_perm)
+  apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))")
+  apply simp
+  apply(rule a)
+  apply assumption
+  done
+
+
 prove alpha1_reflp_aux: {* (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *}
 apply (tactic {*
  (indtac @{thm rtrm1_bp.induct} ["x", "x"] THEN_ALL_NEW
@@ -124,6 +141,14 @@
   rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})
  ) 1 *})
+apply (tactic {*
+ (rtac @{thm alpha_rtrm1_alpha_bp.induct} THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj}) THEN_ALL_NEW
+  TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW
+  (rtac @{thm alpha_gen_atom_sym} THEN' RANGE [
+    (asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt})), atac
+  ])
+ ) 1 *})
 done
 
 lemma alpha1_reflp: