- | Assume of loc * string * nterm * nterm option (* loc, identifier, type, eqty *)
- | Suppose of loc * nterm *string * nterm option (* loc, assumption, identifier, eqass *)
- | By_just_we_proved of loc * just * nterm * string option * nterm option (* loc,
- justification, conclusion, identifier, eqconcl *)
- | We_need_to_prove of loc * nterm * string option * nterm option (* loc, newconclusion,
- identifier, equivnewcon *)
+ | Assume of loc * string * nterm (* loc, identifier, type *)
+ | Suppose of loc * nterm * string (* loc, assumption, identifier *)
+ | By_just_we_proved of loc * just * nterm * string option (* loc, justification, conclusion, identifier *)
+ | We_need_to_prove of loc * nterm * string option (* loc, newconclusion, identifier *)