--- a/Quot/Nominal/Terms.thy	Wed Feb 03 12:44:29 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 03 12:45:06 2010 +0100
@@ -719,7 +719,44 @@
               (pi \<bullet> (bv5 l1) = bv5 l2))
         \<Longrightarrow> rLt5 l1 t1 \<approx>5 rLt5 l2 t2"
 | a4: "rLnil \<approx>l rLnil"
-| a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2"
+| a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> n1 = n2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2"
+
+print_theorems
 
-thm a3[simplified alpha_gen]
+lemma alpha5_inj:
+  "((rVr5 a) \<approx>5 (rVr5 b)) = (a = b)"
+  "(rAp5 t1 s1 \<approx>5 rAp5 t2 s2) = (t1 \<approx>5 t2 \<and> s1 \<approx>5 s2)"
+  "(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = (\<exists>pi. ((bv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (bv5 l2, t2) \<and>
+         (bv5 l1, l1) \<approx>gen alphalts rfv_lts pi (bv5 l2, l2) \<and>
+         (pi \<bullet> (bv5 l1) = bv5 l2)))"
+  "rLnil \<approx>l rLnil"
+  "(rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2) = (ls1 \<approx>l ls2 \<and> t1 \<approx>5 t2 \<and> n1 = n2)"
+apply -
+apply (simp_all add: alpha5_alphalts.intros)
+apply rule
+apply (erule alpha5.cases)
+apply (simp_all add: alpha5_alphalts.intros)
+apply rule
+apply (erule alpha5.cases)
+apply (simp_all add: alpha5_alphalts.intros)
+apply rule
+apply (erule alpha5.cases)
+apply (simp_all add: alpha5_alphalts.intros)
+apply rule
+apply (erule alphalts.cases)
+apply (simp_all add: alpha5_alphalts.intros)
+done
+
+lemma alpha5_equivps:
+  shows "equivp alpha5"
+  and   "equivp alphalts"
+sorry
+
+quotient_type
+  trm5 = rtrm5 / alpha5
+and
+  lts = rlts / alphalts
+  by (auto intro: alpha5_equivps)
+
+
 end