sig
  type t = { carrier : EConstr.constr; r : EConstr.constr; }
  val make : EConstr.constr -> EConstr.constr -> Coq.Relation.t
  val split : Coq.Relation.t -> EConstr.constr * EConstr.constr
end