22   using [[simproc del: alpha_lst]]

    22   using [[simproc del: alpha_lst]]

    23   apply(auto simp add: lt.distinct lt.eq_iff)

    23   apply(auto simp add: lt.distinct lt.eq_iff)

    24   apply(rule_tac y="a" and c="(aa, b)" in lt.strong_exhaust)

    24   apply(rule_tac y="a" and c="(aa, b)" in lt.strong_exhaust)

    25   apply blast

    25   apply blast

    26   apply(simp_all add: fresh_star_def fresh_Pair_elim)

    26   apply(simp_all add: fresh_star_def fresh_Pair_elim)

    28   apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)

    27   apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)

    29   apply(simp add: Abs_fresh_iff)

    28   apply(simp add: Abs_fresh_iff)

    30   apply(simp add: fresh_star_def fresh_Pair)

    29   apply(simp add: fresh_star_def fresh_Pair)

    31   apply(simp add: eqvt_at_def)

    30   apply(simp add: eqvt_at_def)

    32   apply(simp add: perm_supp_eq fresh_star_Pair)

    31   apply(simp add: perm_supp_eq fresh_star_Pair)