244 inductive

   245     alpha2 :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)

   246 where

   247   a1: "a = b \<Longrightarrow> (rVar a) \<approx>2 (rVar b)"

   248 | a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx>2 rApp t2 s2"

   249 | 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"

   250 

   251 lemma 

   252   assumes a1: "t \<approx>2 s"

   253   shows "t \<approx> s"

   254 using a1

   255 apply(induct)

   256 apply(rule alpha.intros)

   257 apply(simp)

   258 apply(rule alpha.intros)

   259 apply(simp)

   260 apply(simp)

   261 apply(rule alpha.intros)

   262 apply(erule disjE)

   263 apply(rule_tac x="0" in exI)

   264 apply(simp add: fresh_star_def fresh_zero_perm)

   265 apply(erule conjE)+

   266 apply(drule alpha_rfv)

   267 apply(simp)

   268 apply(rule_tac x="(a \<leftrightarrow> b)" in exI)

   269 apply(simp)

   270 apply(erule conjE)+

   271 apply(rule conjI)

   272 apply(drule alpha_rfv)

   273 apply(drule sym)

   274 apply(simp)

   275 defer

   276 apply(subgoal_tac "atom a \<sharp> (rfv t - {atom a})")

   277 apply(subgoal_tac "atom b \<sharp> (rfv t - {atom a})")

   278 defer

   279 sorry

   280 

   281 lemma 

   282   assumes a1: "t \<approx> s"

   283   shows "t \<approx>2 s"

   284 using a1

   285 apply(induct)

   286 apply(rule alpha2.intros)

   287 apply(simp)

   288 apply(rule alpha2.intros)

   289 apply(simp)

   290 apply(simp)

   291 apply(clarify)

   292 apply(rule alpha2.intros)

   293 apply(frule alpha_rfv)

   294 apply(rotate_tac 4)

   295 apply(drule sym)

   296 apply(simp)

   297 apply(drule sym)

   298 apply(simp)

   299 apply(case_tac "a = pi \<bullet> a")

   300 apply(simp)

   301 defer

   302 apply(simp)

   303 sorry