diff -r e3ac56d3b7af -r 87894b5156f4 Nominal/Term5.thy
--- a/Nominal/Term5.thy	Mon Mar 01 07:46:50 2010 +0100
+++ b/Nominal/Term5.thy	Mon Mar 01 11:40:48 2010 +0100
@@ -172,6 +172,18 @@
 apply (simp add: permute_trm5_lts fresh_star_def)
 done
 
+lemma lets_ok3:
+  "(Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) =
+   (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
+apply (subst alpha5_INJ)
+apply (rule conjI)
+apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+apply (simp only: alpha_gen)
+apply (simp add: permute_trm5_lts fresh_star_def)
+apply (rule_tac x="0 :: perm" in exI)
+apply (simp only: alpha_gen)
+apply (simp add: permute_trm5_lts fresh_star_def)
+done
 
 lemma lets_not_ok1:
   "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>