72   apply (simp_all add: alpha1_eqvt)

    72   apply (simp_all add: alpha1_eqvt)

    73   apply (subst permute_minus_cancel(2)[symmetric,of "a" "pi"])

    73   apply (subst permute_minus_cancel(2)[symmetric,of "a" "pi"])

    74   apply (subst permute_minus_cancel(2)[symmetric,of "b" "pi"])

    74   apply (subst permute_minus_cancel(2)[symmetric,of "b" "pi"])

    75   apply (simp_all only: alpha1_eqvt)

    75   apply (simp_all only: alpha1_eqvt)

    76 done

    76 done

    77 

    78 

    78 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []),

    79 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []),

    79   (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} ctxt)) ctxt)) *}

    80   (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} ctxt)) ctxt)) *}

    80 thm alpha1_equivp

    81 thm alpha1_equivp

    81 

    82