84   apply (simp)

    84   apply (simp)

    85   apply(rule TrueI)

    85   apply(rule TrueI)

    86   apply (erule lt.exhaust)

    86   apply (erule lt.exhaust)

    87   using [[simproc del: alpha_lst]]

    87   using [[simproc del: alpha_lst]]

    88   apply (simp_all)

    88   apply (simp_all)

    90   apply (simp add: Abs1_eq_iff CPS.eqvt)

    89   apply (simp add: Abs1_eq_iff CPS.eqvt)

    91   by blast

    90   by blast

    92 

    91 

    93 termination (eqvt)

    92 termination (eqvt)

    94   by (relation "measure size") (simp_all)

    93   by (relation "measure size") (simp_all)