sig
  type proof
  module Term :
    sig
      type t
      val equal : Expr_intf.S.Term.t -> Expr_intf.S.Term.t -> bool
      val hash : Expr_intf.S.Term.t -> int
      val print : Format.formatter -> Expr_intf.S.Term.t -> unit
    end
  module Formula :
    sig
      type t
      val equal : Expr_intf.S.Formula.t -> Expr_intf.S.Formula.t -> bool
      val hash : Expr_intf.S.Formula.t -> int
      val print : Format.formatter -> Expr_intf.S.Formula.t -> unit
      val dummy : Expr_intf.S.Formula.t
      val neg : Expr_intf.S.Formula.t -> Expr_intf.S.Formula.t
      val norm :
        Expr_intf.S.Formula.t -> Expr_intf.S.Formula.t * Expr_intf.negated
    end
end