--- a/Quot/Nominal/Terms.thy	Thu Feb 18 18:33:53 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Fri Feb 19 10:17:35 2010 +0100
@@ -1,5 +1,5 @@
 theory Terms
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "../../Attic/Prove"
 begin
 
 atom_decl name
@@ -38,6 +38,9 @@
   alpha_bp ("_ \<approx>1b _" [100, 100] 100)
 thm alpha_rtrm1_alpha_bp.intros
 
+prove {* build_alpha_inj_gl @{thms alpha_rtrm1_alpha_bp.intros} @{context} *}
+sorry
+
 lemma alpha1_inj:
 "(rVr1 a \<approx>1 rVr1 b) = (a = b)"
 "(rAp1 t1 s1 \<approx>1 rAp1 t2 s2) = (t1 \<approx>1 t2 \<and> s1 \<approx>1 s2)"