sig
  type t
  module E :
    sig
      type t =
          Libzipperposition.FOTerm.t * Libzipperposition.FOTerm.t * bool *
          C.t
      type rhs = Libzipperposition.FOTerm.t
      val compare : t -> t -> int
      val extract : t -> Libzipperposition.Index_intf.term * rhs * bool
      val priority : t -> int
    end
  type rhs = E.rhs
  val empty : unit -> t
  val is_empty : t -> bool
  val add : t -> E.t -> t
  val add_seq : t -> E.t Sequence.t -> t
  val add_list : t -> E.t list -> t
  val remove : t -> E.t -> t
  val remove_seq : t -> E.t Sequence.t -> t
  val size : t -> int
  val iter : t -> (Libzipperposition.Index_intf.term -> E.t -> unit) -> unit
  val retrieve :
    ?subst:Libzipperposition.Index_intf.subst ->
    sign:bool ->
    t Libzipperposition.Scoped.t ->
    Libzipperposition.Index_intf.term Libzipperposition.Scoped.t ->
    (Libzipperposition.Index_intf.term * rhs * E.t *
     Libzipperposition.Index_intf.subst)
    Sequence.t
  val to_dot : t CCFormat.printer
end