--- a/Quot/Nominal/Terms.thy	Wed Feb 03 14:39:19 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 03 15:17:29 2010 +0100
@@ -906,6 +906,25 @@
 apply (simp add: insert_eqvt eqvts atom_eqvt)
 done
 
+lemma lets_ok2:
+  "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
+     (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
+apply (subst alpha5_INJ)
+apply (simp add: alpha_gen)
+apply (simp add: permute_trm5_lts fresh_star_def)
+apply (rule allI)
+apply (subst alpha5_INJ)
+apply (subst alpha5_INJ)
+apply (subst alpha5_INJ)
+apply (simp add: insert_eqvt eqvts atom_eqvt)
+apply (subst alpha5_INJ(5))
+apply (subst alpha5_INJ)
+apply (subst alpha5_INJ(5))
+apply (subst alpha5_INJ)
+apply (rule impI)+
+apply (simp)
+done
+
 text {* type schemes *} 
 datatype ty = 
   Var "name"