sig
  type t
  val lemmas :
    MetaProverState_intf.S.Result.t -> MetaProverState_intf.S.lemma list
  val theories :
    MetaProverState_intf.S.Result.t -> MetaProverState_intf.S.theory list
  val axioms :
    MetaProverState_intf.S.Result.t -> MetaProverState_intf.S.axiom list
  val rewrite :
    MetaProverState_intf.S.Result.t -> MetaProverState_intf.S.rewrite list
  val pre_rewrite :
    MetaProverState_intf.S.Result.t ->
    MetaProverState_intf.S.pre_rewrite list
  val print : Format.formatter -> MetaProverState_intf.S.Result.t -> unit
end