justification, conclusion, identifier, eqconcl *)
| We_need_to_prove of loc * nterm * string option * nterm option (* loc, newconclusion,
identifier, equivnewcon *)
justification, conclusion, identifier, eqconcl *)
| We_need_to_prove of loc * nterm * string option * nterm option (* loc, newconclusion,
identifier, equivnewcon *)