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