sig
  module Loc = Logtk.ParseLocation
  type form = Logtk.TypedSTerm.t
  type bool_lit = BBox.Lit.t
  type 'a sequence = ('a -> unit) -> unit
  val section : Logtk.Util.Section.t
  type statement_src = Logtk.Statement.source
  type rule
  type check = [ `Check | `Check_with of Proof.form list | `No_check ]
  type kind =
      Inference of Proof.rule * Proof.check
    | Simplification of Proof.rule * Proof.check
    | Esa of Proof.rule * Proof.check
    | Assert of Proof.statement_src
    | Goal of Proof.statement_src
    | Lemma
    | Data of Proof.statement_src * Logtk.Type.t Logtk.Statement.data
    | Trivial
    | By_def of Logtk.ID.t
  type result =
      Form of Proof.form
    | Clause of SClause.t
    | BoolClause of Proof.bool_lit list
    | Stmt of Logtk.Statement.input_t
    | C_stmt of Logtk.Statement.clause_t
  type step
  type proof
  type t = Proof.proof
  type parent
  type info = Logtk.UntypedAST.attr
  type infos = Proof.info list
  module Rule :
    sig
      type t = Proof.rule
      val pp : Proof.Rule.t CCFormat.printer
      val name : Proof.Rule.t -> string
      val mk : string -> Proof.Rule.t
      val mkf :
        ('a, Format.formatter, unit, Proof.Rule.t) Pervasives.format4 -> 'a
    end
  module Kind :
    sig type t = Proof.kind val pp : Proof.Kind.t CCFormat.printer end
  module Result :
    sig
      type t = Proof.result
      val compare : t -> t -> int
      val equal : t -> t -> bool
      val pp : Proof.Result.t CCFormat.printer
    end
  module Step :
    sig
      type t = Proof.step
      val kind : Proof.Step.t -> Proof.kind
      val parents : Proof.Step.t -> Proof.parent list
      val infos : Proof.Step.t -> Proof.infos
      val compare : Proof.Step.t -> Proof.Step.t -> int
      val hash : Proof.Step.t -> int
      val equal : Proof.Step.t -> Proof.Step.t -> bool
      val trivial : Proof.Step.t
      val by_def : Logtk.ID.t -> Proof.Step.t
      val data :
        Proof.statement_src ->
        Logtk.Type.t Logtk.Statement.data -> Proof.Step.t
      val assert_ : Proof.statement_src -> Proof.Step.t
      val goal : Proof.statement_src -> Proof.Step.t
      val lemma : Proof.Step.t
      val assert' :
        ?loc:Loc.t -> file:string -> name:string -> unit -> Proof.Step.t
      val goal' :
        ?loc:Loc.t -> file:string -> name:string -> unit -> Proof.Step.t
      val inference :
        ?infos:Proof.infos ->
        ?check:Proof.check ->
        rule:Proof.rule -> Proof.parent list -> Proof.Step.t
      val simp :
        ?infos:Proof.infos ->
        ?check:Proof.check ->
        rule:Proof.rule -> Proof.parent list -> Proof.Step.t
      val esa :
        ?infos:Proof.infos ->
        ?check:Proof.check ->
        rule:Proof.rule -> Proof.parent list -> Proof.Step.t
      val is_trivial : Proof.Step.t -> bool
      val is_by_def : Proof.Step.t -> bool
      val is_assert : Proof.Step.t -> bool
      val is_goal : Proof.Step.t -> bool
      val rule : Proof.Step.t -> Proof.rule option
      val distance_to_goal : Proof.Step.t -> int option
      val pp : Proof.Step.t CCFormat.printer
    end
  module Parent :
    sig
      type t = Proof.parent
      val from : Proof.proof -> Proof.Parent.t
      val from_subst :
        Proof.proof Logtk.Scoped.t -> Logtk.Subst.t -> Proof.Parent.t
      val add_subst :
        Proof.Parent.t Logtk.Scoped.t -> Logtk.Subst.t -> Proof.Parent.t
      val proof : Proof.Parent.t -> Proof.proof
      val subst : Proof.Parent.t -> Logtk.Subst.t list
    end
  module S :
    sig
      type t = Proof.proof
      val result : Proof.S.t -> Proof.result
      val step : Proof.S.t -> Proof.step
      val compare : Proof.S.t -> Proof.S.t -> int
      val equal : Proof.S.t -> Proof.S.t -> bool
      val hash : Proof.S.t -> int
      val compare_by_result : Proof.S.t -> Proof.S.t -> int
      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
      val mk_f : Proof.step -> Proof.form -> Proof.S.t
      val mk_f_trivial : Proof.form -> Proof.S.t
      val mk_f_by_def : Logtk.ID.t -> Proof.form -> Proof.S.t
      val mk_f_inference :
        ?check:Proof.check ->
        rule:Proof.rule -> Proof.form -> Proof.parent list -> Proof.S.t
      val mk_f_simp :
        ?check:Proof.check ->
        rule:Proof.rule -> Proof.form -> Proof.parent list -> Proof.S.t
      val mk_f_esa :
        ?check:Proof.check ->
        rule:Proof.rule -> Proof.form -> Proof.parent list -> Proof.S.t
      val mk_c : Proof.step -> SClause.t -> Proof.S.t
      val mk_bc : Proof.step -> Proof.bool_lit list -> Proof.S.t
      val mk_stmt : Proof.step -> Logtk.Statement.input_t -> Proof.S.t
      val adapt_f : Proof.S.t -> Proof.form -> Proof.S.t
      val adapt_c : Proof.S.t -> SClause.t -> Proof.S.t
      val to_llproof : Proof.S.t -> Logtk.LLProof.t
      val is_proof_of_false : Proof.S.t -> bool
      val as_graph :
        (Proof.S.t, Proof.rule * Logtk.Subst.t list * Proof.infos) CCGraph.t
      val traverse :
        ?traversed:unit Proof.S.Tbl.t ->
        order:[ `BFS | `DFS ] -> Proof.S.t -> Proof.S.t Sequence.t
      val pp_result_of : Proof.S.t CCFormat.printer
      val pp_notrec : Proof.S.t CCFormat.printer
      val pp_tstp : Proof.S.t CCFormat.printer
      val pp_normal : Proof.S.t CCFormat.printer
      val pp_zf : Proof.S.t CCFormat.printer
      val pp : Logtk.Options.print_format -> Proof.S.t CCFormat.printer
      val pp_dot : name:string -> Proof.S.t CCFormat.printer
      val pp_dot_file : ?name:string -> string -> Proof.S.t -> unit
      val pp_dot_seq : name:string -> Proof.S.t Sequence.t CCFormat.printer
      val pp_dot_seq_file :
        ?name:string -> string -> Proof.S.t Sequence.t -> unit
      val step_of_src : Logtk.Statement.Src.t -> Proof.Step.t
      val parent_of_sourced : Logtk.Statement.sourced_t -> Proof.Parent.t
    end
end