148 

   148 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))"

   149 

   149   apply (rule equ_trans)

   150 

   150   apply (rule equ_App1)

   151   apply (rule equ_beta)

   152   apply (simp add: lam.fresh fresh_at_base)

   153   apply (subst subst.simps)

   154   apply (simp add: lam.fresh fresh_at_base)+

   155   apply (rule equ_trans)

   156   apply (rule equ_beta)

   157   apply (simp add: lam.fresh fresh_at_base)

   158   apply (simp add: equ_refl)

   159   done

   160 

   161 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))"

   162   apply rule

   163   apply (erule equ2.cases)

   164   apply auto

   165   done