sig
type t =
Axiom
| Resolved of Reasoner.fact Reasoner.Proof.with_proof *
Reasoner.clause Reasoner.Proof.with_proof
and 'a with_proof = { conclusion : 'a; proof : Reasoner.Proof.t; }
val facts : Reasoner.Proof.t -> Reasoner.fact Sequence.t
val rules : Reasoner.Proof.t -> Reasoner.clause Sequence.t
end