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