sig
  type bool_lit = BBox.Lit.t
  type t = Bool_clause.bool_lit list
  val proof_tc : Bool_clause.t Logtk.Proof.Result.tc
  val mk_proof_res : Bool_clause.t -> Logtk.Proof.Result.t
  exception E_proof of Bool_clause.t
  val proof_res_as_bc : Logtk.Proof.Result.t -> Bool_clause.t option
end