"elim_type eqt su t1 ...", ProofEngineTypes.mk_tactic (fun status ->
let status' = (* status after 1st elim_type use *)
let context = context_of_status status in
"elim_type eqt su t1 ...", ProofEngineTypes.mk_tactic (fun status ->
let status' = (* status after 1st elim_type use *)
let context = context_of_status status in