302 lemma real_alpha_pre:

   303   assumes a: "t = [(a,b)]\<bullet>s" "a\<sharp>[b].s"

   304   shows "rLam a t \<approx> rLam b s"

   305 sorry

   306 

   307 lemma perm_prs : "(id ---> option_map ABS_lam) ([b].REP_lam s) = [b].s"

   308 sorry

   309 

   310 lemma perm_prs2: "(id ---> option_map ABS_lam) ((id ---> option_map REP_lam) ([b].(s::lam))) = [b].s"

   311 sorry

   312 

   313 lemma real_alpha:

   314   "\<lbrakk>t = [(a, b)] \<bullet> s; a \<sharp> [b].s\<rbrakk> \<Longrightarrow> Lam a t = Lam b s"

   315 apply (tactic {* procedure_tac @{context} @{thm real_alpha_pre} 1 *})

   316 prefer 2

   317 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})

   318 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})

   319 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})

   320 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})

   321 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})

   322 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})

   323 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})

   324 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})

   325 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})

   326 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})

   327 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})

   328 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})

   329 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})

   330 apply (tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})

   331 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})

   332 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})

   333 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})

   334 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})

   335 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})

   336 apply (simp only: perm_prs)

   337 prefer 2

   338 apply (tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})

   339 prefer 3

   340 apply (tactic {* clean_tac @{context} [quot] defs 1 *})

   341 

   342 thm all_prs

   343 thm REP_ABS_RSP

   344 thm ball_reg_eqv_range

   345 

   346 

   347 thm perm_lam_def

   348 apply (simp only: perm_prs)

   349 

   350 apply (tactic {* regularize_tac @{context} [quot] 1 *})

   351 

   352 done

   353