diff -r 9c968284553c -r fb33684e4ece Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Mon Feb 22 10:57:39 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Mon Feb 22 12:12:32 2010 +0100
@@ -116,9 +116,27 @@
   apply(simp add: permute_eqvt[symmetric])
   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
+  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 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 *})
+done
+
+lemma alpha1_reflp: 
+  "reflp alpha_rtrm1"
+  "reflp alpha_bp"
+unfolding reflp_def
+apply (simp_all add: alpha1_reflp_aux)
+done
+
 lemma alpha1_equivp: "equivp alpha_rtrm1" 
   sorry
 
+
 quotient_type trm1 = rtrm1 / alpha_rtrm1
   by (rule alpha1_equivp)