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