# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265206649 -3600
# Node ID a9135d300fbfc1556cd8de487e53e773dd494d32
# Parent  34220518cccf24b0a424fbba4c23d81423f137ca
Lets different.

diff -r 34220518cccf -r a9135d300fbf Quot/Nominal/Terms.thy
--- 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"