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