--- a/Quot/Nominal/Fv.thy	Mon Feb 22 12:12:32 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Mon Feb 22 13:41:13 2010 +0100
@@ -259,12 +259,15 @@
     let
       val ty = domain_type (fastype_of alpha);
       val var = Free("x", ty);
+      val var2 = Free("y", ty);
     in
-      alpha $ var $ var
-    end
-  val eqs = map build_alpha alphas
+      ((alpha $ var $ var), (HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var)))
+    end;
+  val (refl_eqs, sym_eqs) = split_list (map build_alpha alphas)
 in
-  @{term Trueprop} $ foldr1 HOLogic.mk_conj eqs
+  Logic.mk_conjunction
+  (@{term Trueprop} $ foldr1 HOLogic.mk_conj refl_eqs,
+   @{term Trueprop} $ foldr1 HOLogic.mk_conj sym_eqs)
 end
 *}
 

--- 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: