(*CSC: che si guadagni nulla in fatto di efficienza. *)
let replace =
ProofEngineReduction.replace
- ~equality:(ProofEngineReduction.syntactic_equality)
+ ~equality:
+ (ProofEngineReduction.syntactic_equality ~alpha_equivalence:false)
~what:term' ~with_what:term
in
let ty' = replace ty in