24   apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)

    24   apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)

    25   apply (simp add: fresh_at_base Abs1_eq_iff)

    25   apply (simp add: fresh_at_base Abs1_eq_iff)

    26   apply (case_tac b)

    26   apply (case_tac b)

    27   apply (rule_tac y="a" in lt.strong_exhaust)

    27   apply (rule_tac y="a" in lt.strong_exhaust)

    28   apply auto[3]

    28   apply auto[3]

    30   apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) 

    29   apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) 

    31   apply (simp add: fresh_at_base Abs1_eq_iff)

    30   apply (simp add: fresh_at_base Abs1_eq_iff)

    32 --"-"

    31 --"-"

    33   apply (subgoal_tac "Lam c (ka (c~)) = Lam ca (ka (ca~))")

    32   apply (subgoal_tac "Lam c (ka (c~)) = Lam ca (ka (ca~))")

    34   apply (simp only:)

    33   apply (simp only:)