sig
  type fact
  and proof =
      BuiltinProof
    | InputFactProof
    | Proof of Term.term * Fact.fact array
    | DisjProof of int * Term.term * Fact.fact array * Fact.fact list
    | NegProof of Term.term * Fact.fact array * Fact.fact
    | UnknownProof
  val null_fact : Fact.fact
  val fact_with_unknown_proof : Fact.fact
  val make_input_fact : Term.term -> Fact.fact
  val make_derived_fact : Term.term -> Fact.fact
  val make_derived_fact_with_proof : Term.term -> Fact.proof -> Fact.fact
  val make_fact_like : Fact.fact -> Term.term -> Fact.fact
  type entry = Fact.fact
  val get_term : Fact.fact -> Term.term
  val get_proof : Fact.fact -> Fact.proof
  val proof_term_for_fact : Term.symbol_table -> Fact.fact -> Term.term
  type l_proof = Fact.proof list
  val proof_term_for_l_proof : Term.symbol_table -> Fact.l_proof -> Term.term
  val make_subproofs : int -> Fact.fact array
  type proof_term_aux
  val make_proof_term_aux : unit -> Fact.proof_term_aux
  val proof_term_for_r_proof :
    Term.symbol_table -> Fact.proof_term_aux -> Fact.proof -> Term.term
end