sig
  type t
  module E :
    sig
      type t = FOTerm.t * FOTerm.t
      type rhs = FOTerm.t
      val compare : t -> t -> int
      val extract : t -> 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 -> (Index_intf.term -> E.t -> unit) -> unit
  val retrieve :
    ?subst:Index_intf.subst ->
    sign:bool ->
    t Scoped.t ->
    Index_intf.term Scoped.t ->
    (Index_intf.term * rhs * E.t * Index_intf.subst) Sequence.t
  val to_dot : t CCFormat.printer
end