sig
  val section : Libzipperposition.Util.Section.t
  type rule_term
  val rhs_term : Rewrite_rule.rule_term -> Libzipperposition.FOTerm.t
  val pp_rule_term : Rewrite_rule.rule_term CCFormat.printer
  type rule_clause
  val rhs_clause : Rewrite_rule.rule_clause -> Literal.t list list
  val pp_rule_clause : Rewrite_rule.rule_clause CCFormat.printer
  module Set :
    sig
      type t
      val empty : Rewrite_rule.Set.t
      val is_empty : Rewrite_rule.Set.t -> bool
      val add_stmt :
        Libzipperposition.Statement.clause_t ->
        Rewrite_rule.Set.t -> Rewrite_rule.Set.t
      val pp : Rewrite_rule.Set.t CCFormat.printer
    end
  val normalize_term :
    Rewrite_rule.Set.t ->
    Libzipperposition.FOTerm.t -> Libzipperposition.FOTerm.t
  val narrow_term :
    ?subst:Libzipperposition.Substs.t ->
    Rewrite_rule.Set.t Libzipperposition.Scoped.t ->
    Libzipperposition.FOTerm.t Libzipperposition.Scoped.t ->
    (Rewrite_rule.rule_term * Libzipperposition.Substs.t) Sequence.t
  val normalize_clause :
    Rewrite_rule.Set.t -> Literal.t list -> Literal.t list list option
  val narrow_lit :
    ?subst:Libzipperposition.Substs.t ->
    Rewrite_rule.Set.t Libzipperposition.Scoped.t ->
    Literal.t Libzipperposition.Scoped.t ->
    (Rewrite_rule.rule_clause * Libzipperposition.Substs.t) Sequence.t
end