sig
  type t
  module R : Sig.X
  val empty : Uf.S.t
  val add : Uf.S.t -> Term.t -> Uf.S.t * Literal.LT.t list
  val mem : Uf.S.t -> Term.t -> bool
  val find : Uf.S.t -> Term.t -> R.r * Explanation.t
  val find_r : Uf.S.t -> R.r -> R.r * Explanation.t
  val union :
    Uf.S.t ->
    R.r ->
    R.r ->
    Explanation.t ->
    Uf.S.t * (R.r * (R.r * R.r * Explanation.t) list * R.r) list
  val distinct : Uf.S.t -> R.r list -> Explanation.t -> Uf.S.t
  val are_equal : Uf.S.t -> Term.t -> Term.t -> Sig.answer
  val are_distinct : Uf.S.t -> Term.t -> Term.t -> Sig.answer
  val already_distinct : Uf.S.t -> R.r list -> bool
  val class_of : Uf.S.t -> Term.t -> Term.t list
end