(*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
(*CSC: che si guadagni nulla in fatto di efficienza. *)
let replace = ProofEngineReduction.replace
- ~equality:(==) ~what:term' ~with_what:term
+ ~equality:(=) ~what:term' ~with_what:term
in
let ty' = replace ty in
let context' =