sig
  type t = {
    carrier : EConstr.constr;
    eq : EConstr.constr;
    equivalence : EConstr.constr;
  }
  val make :
    EConstr.constr -> EConstr.constr -> EConstr.constr -> Coq.Equivalence.t
  val infer :
    Environ.env ->
    Evd.evar_map ->
    EConstr.constr -> EConstr.constr -> Coq.Equivalence.t * Evd.evar_map
  val from_relation :
    Environ.env ->
    Evd.evar_map -> Coq.Relation.t -> Coq.Equivalence.t * Evd.evar_map
  val to_relation : Coq.Equivalence.t -> Coq.Relation.t
  val split :
    Coq.Equivalence.t -> EConstr.constr * EConstr.constr * EConstr.constr
end