sig
  val section : Logtk.Util.Section.t
  type inductive_case = Cover_set.case
  type payload = private
      Fresh
    | Clause_component of Logtk.Literals.t
    | Lemma of Cut_form.t
    | Case of BBox.inductive_case list
  module Lit :
    sig
      type t
      type payload = payload
      val compare : t -> t -> int
      val equal : t -> t -> bool
      val hash : t -> int
      val dummy : t
      val neg : t -> t
      val sign : t -> bool
      val abs : t -> t
      val norm : t -> t * bool
      val set_sign : bool -> t -> t
      val apply_sign : bool -> t -> t
      val make : payload -> t
      val payload : t -> payload
      val to_int : t -> int
      val fresh_id : unit -> int
      val pp : t CCFormat.printer
      module Set :
        sig
          type elt = t
          type t
          val empty : t
          val is_empty : t -> bool
          val mem : elt -> t -> bool
          val add : elt -> t -> t
          val singleton : elt -> t
          val remove : elt -> t -> t
          val union : t -> t -> t
          val inter : t -> t -> t
          val diff : t -> t -> t
          val compare : t -> t -> int
          val equal : t -> t -> bool
          val subset : t -> t -> bool
          val iter : (elt -> unit) -> t -> unit
          val map : (elt -> elt) -> t -> t
          val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
          val for_all : (elt -> bool) -> t -> bool
          val exists : (elt -> bool) -> t -> bool
          val filter : (elt -> bool) -> t -> t
          val partition : (elt -> bool) -> t -> t * t
          val cardinal : t -> int
          val elements : t -> elt list
          val min_elt : t -> elt
          val max_elt : t -> elt
          val choose : t -> elt
          val split : elt -> t -> t * bool * t
          val find : elt -> t -> elt
          val of_seq : elt CCSet.sequence -> t
          val add_seq : t -> elt CCSet.sequence -> t
          val to_seq : t -> elt CCSet.sequence
          val of_list : elt list -> t
          val add_list : t -> elt list -> t
          val to_list : t -> elt list
          val pp :
            ?start:string ->
            ?stop:string ->
            ?sep:string -> elt CCSet.printer -> t CCSet.printer
        end
      module Tbl :
        sig
          type key = t
          type 'a t
          val create : int -> 'a t
          val clear : 'a t -> unit
          val reset : 'a t -> unit
          val copy : 'a t -> 'a t
          val add : 'a t -> key -> 'a -> unit
          val remove : 'a t -> key -> unit
          val find : 'a t -> key -> 'a
          val find_all : 'a t -> key -> 'a list
          val replace : 'a t -> key -> 'a -> unit
          val mem : 'a t -> key -> bool
          val iter : (key -> 'a -> unit) -> 'a t -> unit
          val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
          val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
          val length : 'a t -> int
          val stats : 'a t -> Hashtbl.statistics
          val get : 'a t -> key -> 'a option
          val get_or : 'a t -> key -> default:'a -> 'a
          val add_list : 'a list t -> key -> 'a -> unit
          val incr : ?by:int -> int t -> key -> unit
          val decr : ?by:int -> int t -> key -> unit
          val keys : 'a t -> key CCHashtbl.sequence
          val values : 'a t -> 'a CCHashtbl.sequence
          val keys_list : 'a t -> key list
          val values_list : 'a t -> 'a list
          val map_list : (key -> 'a -> 'b) -> 'a t -> 'b list
          val to_seq : 'a t -> (key * 'a) CCHashtbl.sequence
          val of_seq : (key * 'a) CCHashtbl.sequence -> 'a t
          val add_seq : 'a t -> (key * 'a) CCHashtbl.sequence -> unit
          val add_seq_count : int t -> key CCHashtbl.sequence -> unit
          val of_seq_count : key CCHashtbl.sequence -> int t
          val to_list : 'a t -> (key * 'a) list
          val of_list : (key * 'a) list -> 'a t
          val update :
            'a t -> f:(key -> 'a option -> 'a option) -> k:key -> unit
          val get_or_add : 'a t -> f:(key -> 'a) -> k:key -> 'a
          val print :
            key CCHashtbl.printer ->
            'a CCHashtbl.printer -> 'a t CCHashtbl.printer
        end
    end
  type t = BBox.Lit.t
  val dummy : BBox.t
  val pp_payload : BBox.payload CCFormat.printer
  val inject_lits : Logtk.Literals.t -> BBox.t
  val inject_lemma : Cut_form.t -> BBox.t
  val inject_case : BBox.inductive_case list -> BBox.t
  val payload : BBox.t -> BBox.payload
  val is_case : BBox.t -> bool
  val as_case : BBox.t -> BBox.inductive_case list option
  val as_lemma : BBox.t -> Cut_form.t option
  val must_be_kept : BBox.t -> bool
  val is_lemma : BBox.t -> bool
  val to_s_form : BBox.t -> Logtk.TypedSTerm.Form.t
  val pp : BBox.t CCFormat.printer
  val pp_tstp : BBox.t CCFormat.printer
  val pp_zf : BBox.t CCFormat.printer
  val pp_bclause : BBox.t list CCFormat.printer
end