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