sig
  type t
  type rhs
  val compare : Index_intf.EQUATION.t -> Index_intf.EQUATION.t -> int
  val extract :
    Index_intf.EQUATION.t -> Index_intf.term * Index_intf.EQUATION.rhs * bool
  val priority : Index_intf.EQUATION.t -> int
end