63 

    63 

    64 local_setup {*

    64 local_setup {*

    65 (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt}, []),

    65 (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt}, []),

    66   build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms perm_fixed alpha4_inj} ctxt 1) ctxt) ctxt))

    66   build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms perm_fixed alpha4_inj} ctxt 1) ctxt) ctxt))

    67 *}

    67 *}

    68 thm alpha4_eqvt

    70 thm alpha4_eqvt

    69 lemmas alpha4_eqvt_fixed = alpha4_eqvt(1)[simplified alpha_fix (*fv_fix*)]

    71 lemmas alpha4_eqvt_fixed = alpha4_eqvt(1)[simplified alpha_fix (*fv_fix*)]

    70 

    72 

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

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

    72   build_alpha_refl [((0, @{term alpha_rtrm4}), 0), ((0, @{term alpha_rtrm4_list}), 0)] [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thms alpha4_inj} ctxt) ctxt)) *}

    74   build_alpha_refl [((0, @{term alpha_rtrm4}), 0), ((0, @{term alpha_rtrm4_list}), 0)] [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thms alpha4_inj} ctxt) ctxt)) *}