sig
  type t
  type elt
  val empty : Index_intf.LEAF.t
  val add :
    Index_intf.LEAF.t ->
    Index_intf.term -> Index_intf.LEAF.elt -> Index_intf.LEAF.t
  val remove :
    Index_intf.LEAF.t ->
    Index_intf.term -> Index_intf.LEAF.elt -> Index_intf.LEAF.t
  val is_empty : Index_intf.LEAF.t -> bool
  val iter :
    Index_intf.LEAF.t ->
    (Index_intf.term -> Index_intf.LEAF.elt -> unit) -> unit
  val fold :
    Index_intf.LEAF.t ->
    'a -> ('a -> Index_intf.term -> Index_intf.LEAF.elt -> 'a) -> 'a
  val size : Index_intf.LEAF.t -> int
  val fold_unify :
    ?subst:Index_intf.subst ->
    Index_intf.LEAF.t Scoped.t ->
    Index_intf.term Scoped.t ->
    (Index_intf.term * Index_intf.LEAF.elt * Index_intf.subst) Sequence.t
  val fold_match :
    ?subst:Index_intf.subst ->
    Index_intf.LEAF.t Scoped.t ->
    Index_intf.term Scoped.t ->
    (Index_intf.term * Index_intf.LEAF.elt * Index_intf.subst) Sequence.t
  val fold_matched :
    ?subst:Index_intf.subst ->
    Index_intf.LEAF.t Scoped.t ->
    Index_intf.term Scoped.t ->
    (Index_intf.term * Index_intf.LEAF.elt * Index_intf.subst) Sequence.t
end