let lapply_tac_aux ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
(* ?(substs = []) *) ?how_many ?(to_what = []) what =
let letin_tac term = PT.letin_tac ~mk_fresh_name_callback term in
let lapply_tac (proof, goal) =
let lapply_tac_aux ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
(* ?(substs = []) *) ?how_many ?(to_what = []) what =
let letin_tac term = PT.letin_tac ~mk_fresh_name_callback term in
let lapply_tac (proof, goal) =