sig
  val to_seq : Prover.t -> Reasoner.clause Sequence.t
  val of_seq :
    Prover.t ->
    Reasoner.clause Sequence.t -> Prover.t * Reasoner.consequence Sequence.t
end