sig
  val section : Libzipperposition.Util.Section.t
  type inductive_path = Ind_cst.path
  type payload = private
      Fresh
    | Clause_component of Literals.t
    | Lemma of Literals.t list
    | Case of BBox.inductive_path
  module Lit :
    sig
      type t
      type payload = payload
      val compare : t -> t -> int
      val equal : t -> t -> bool
      val hash : t -> int
      val hash_fun : t CCHash.hash_fun
      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 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
          val print :
            ?start:string ->
            ?stop:string ->
            ?sep:string -> elt CCSet.formatter -> t CCSet.formatter
        end
    end
  type t = BBox.Lit.t
  val dummy : BBox.t
  val pp_payload : BBox.payload CCFormat.printer
  val inject_lits : Literals.t -> BBox.t
  val inject_lemma : Literals.t list -> BBox.t
  val inject_case : BBox.inductive_path -> BBox.t
  val payload : BBox.t -> BBox.payload
  val as_case : BBox.t -> BBox.inductive_path option
  val must_be_kept : BBox.t -> bool
  val pp : BBox.t CCFormat.printer
  val pp_bclause : BBox.t list CCFormat.printer
end