sig
  val mk_morphism :
    EConstr.constr -> EConstr.constr -> EConstr.constr -> EConstr.constr
  val mk_equivalence : EConstr.constr -> EConstr.constr -> EConstr.constr
  val mk_reflexive : EConstr.constr -> EConstr.constr -> EConstr.constr
  val mk_transitive : EConstr.constr -> EConstr.constr -> EConstr.constr
end