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