(* the type of one metavariable. So we replace it everywhere. *)
(*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
+ let replace =
+ ProofEngineReduction.replace
+ ~equality:(ProofEngineReduction.syntactic_equality)
+ ~what:term' ~with_what:term
in
let ty' = replace ty in
let context' =