tactic.generalize_proofs source