--- a/Nominal/Ex/Beta.thy	Thu Dec 15 16:20:42 2011 +0000
+++ b/Nominal/Ex/Beta.thy	Fri Dec 16 16:01:12 2011 +0900
@@ -145,9 +145,24 @@
 apply(auto)
 oops
 
-
+lemma "a \<noteq> x \<Longrightarrow> x \<noteq> y \<Longrightarrow> y \<noteq> a \<Longrightarrow> y \<noteq> b \<Longrightarrow> (App (App (Lam[x]. Lam[y]. (App (Var y) (Var x))) (Var a)) (Var b) \<approx> App (Var b) (Var a))"
+  apply (rule equ_trans)
+  apply (rule equ_App1)
+  apply (rule equ_beta)
+  apply (simp add: lam.fresh fresh_at_base)
+  apply (subst subst.simps)
+  apply (simp add: lam.fresh fresh_at_base)+
+  apply (rule equ_trans)
+  apply (rule equ_beta)
+  apply (simp add: lam.fresh fresh_at_base)
+  apply (simp add: equ_refl)
+  done
 
-
+lemma "\<not> (Var b \<approx>2 Var a) \<Longrightarrow> \<not> (App (App (Lam[x]. Lam[y]. (App (Var y) (Var x))) (Var a)) (Var b) \<approx>2 App (Var b) (Var a))"
+  apply rule
+  apply (erule equ2.cases)
+  apply auto
+  done
 
 lemma [quot_respect]:
   shows "(op = ===> equ) Var Var"