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