91  |> snd o (Quotient_Def.quotient_lift_const ("fv_trm", @{term fv_rtrm}))) *}

    91  |> snd o (Quotient_Def.quotient_lift_const ("fv_trm", @{term fv_rtrm}))) *}

    92 print_theorems

    92 print_theorems

    93 

    93 

    94 local_setup {* snd o prove_const_rsp @{binding rfv_rsp} [@{term fv_rkind}, @{term fv_rty}, @{term fv_rtrm}]

    94 local_setup {* snd o prove_const_rsp @{binding rfv_rsp} [@{term fv_rkind}, @{term fv_rty}, @{term fv_rtrm}]

    95   (fn _ => fvbv_rsp_tac @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} @{thms fv_rkind_fv_rty_fv_rtrm.simps} 1) *}

    95   (fn _ => fvbv_rsp_tac @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} @{thms fv_rkind_fv_rty_fv_rtrm.simps} 1) *}

   101   (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *}

    97   (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *}

   102 ML {* fun const_rsp_tac _ = constr_rsp_tac @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj}

    98 ML {* fun const_rsp_tac _ = constr_rsp_tac @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj}

   103   @{thms rfv_rsp} @{thms alpha_equivps} 1 *}

    99   @{thms rfv_rsp} @{thms alpha_equivps} 1 *}

   104 local_setup {* snd o prove_const_rsp Binding.empty [@{term TConst}] const_rsp_tac *}

   100 local_setup {* snd o prove_const_rsp Binding.empty [@{term TConst}] const_rsp_tac *}

   105 local_setup {* snd o prove_const_rsp Binding.empty [@{term TApp}] const_rsp_tac *}

   101 local_setup {* snd o prove_const_rsp Binding.empty [@{term TApp}] const_rsp_tac *}