let left = call_tactic ProofEngine.left
let right = call_tactic ProofEngine.right
let assumption = call_tactic ProofEngine.assumption
+ let injection = call_tactic_with_input ProofEngine.injection
+ let discriminate = call_tactic_with_input ProofEngine.discriminate
let generalize =
call_tactic_with_goal_inputs
(ProofEngine.generalize ~mk_fresh_name_callback:C.mk_fresh_name_callback)