module Leibniz: sig .. end
sig
end
val eq_refl : EConstr.types -> EConstr.constr -> EConstr.constr
EConstr.types -> EConstr.constr -> EConstr.constr