--- a/Quot/Nominal/LamEx.thy	Thu Jan 28 12:28:50 2010 +0100
+++ b/Quot/Nominal/LamEx.thy	Thu Jan 28 14:20:26 2010 +0100
@@ -241,6 +241,66 @@
   apply(simp_all)
   done
 
+inductive
+    alpha2 :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)
+where
+  a1: "a = b \<Longrightarrow> (rVar a) \<approx>2 (rVar b)"
+| a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx>2 rApp t2 s2"
+| a3: "(a = b \<and> t \<approx>2 s) \<or> (a \<noteq> b \<and> ((a \<leftrightarrow> b) \<bullet> t) \<approx>2 s \<and> atom b \<notin> rfv t)\<Longrightarrow> rLam a t \<approx>2 rLam b s"
+
+lemma 
+  assumes a1: "t \<approx>2 s"
+  shows "t \<approx> s"
+using a1
+apply(induct)
+apply(rule alpha.intros)
+apply(simp)
+apply(rule alpha.intros)
+apply(simp)
+apply(simp)
+apply(rule alpha.intros)
+apply(erule disjE)
+apply(rule_tac x="0" in exI)
+apply(simp add: fresh_star_def fresh_zero_perm)
+apply(erule conjE)+
+apply(drule alpha_rfv)
+apply(simp)
+apply(rule_tac x="(a \<leftrightarrow> b)" in exI)
+apply(simp)
+apply(erule conjE)+
+apply(rule conjI)
+apply(drule alpha_rfv)
+apply(drule sym)
+apply(simp)
+defer
+apply(subgoal_tac "atom a \<sharp> (rfv t - {atom a})")
+apply(subgoal_tac "atom b \<sharp> (rfv t - {atom a})")
+defer
+sorry
+
+lemma 
+  assumes a1: "t \<approx> s"
+  shows "t \<approx>2 s"
+using a1
+apply(induct)
+apply(rule alpha2.intros)
+apply(simp)
+apply(rule alpha2.intros)
+apply(simp)
+apply(simp)
+apply(clarify)
+apply(rule alpha2.intros)
+apply(frule alpha_rfv)
+apply(rotate_tac 4)
+apply(drule sym)
+apply(simp)
+apply(drule sym)
+apply(simp)
+apply(case_tac "a = pi \<bullet> a")
+apply(simp)
+defer
+apply(simp)
+sorry
 
 quotient_type lam = rlam / alpha
   by (rule alpha_equivp)