258          ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)"

   258          ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)"

   259 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11

   259 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11

   260 apply - 

   260 apply - 

   261 apply(tactic {* lift_tac @{context} @{thm akind_aty_atrm.induct} @{thms alpha_EQUIVs} 1 *})

   261 apply(tactic {* lift_tac @{context} @{thm akind_aty_atrm.induct} @{thms alpha_EQUIVs} 1 *})

   262 (*apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})

   262 (*apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})

   264 apply(tactic {* clean_tac @{context} 1 *})

   264 apply(tactic {* clean_tac @{context} 1 *})

   265 *)

   265 *)

   266 (*apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})*)

   266 (*apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})*)

   267 (*

   267 (*

   268 Profiling:

   268 Profiling: