functor (I : EQ) ->
  functor
    (L : sig
           type t = I.e
           val level : Trace.level
           val eq : Infsys.LEVEL.t -> Infsys.LEVEL.t -> bool
           val diff : Infsys.LEVEL.t -> Infsys.LEVEL.t -> Infsys.LEVEL.t
           val pp : Infsys.LEVEL.t Pretty.printer
         end) ->
    sig
      type e = I.e
      val current : unit -> Infsys.EQ.e
      val initialize : Infsys.EQ.e -> unit
      val finalize : unit -> Infsys.EQ.e
      val abstract : Term.t -> unit
      val merge : Fact.Equal.t -> unit
      val propagate : Fact.Equal.t -> unit
      val dismerge : Fact.Diseq.t -> unit
      val propagate_diseq : Fact.Diseq.t -> unit
      val branch : unit -> unit
      val normalize : unit -> unit
    end