Module Reasoner.Proof

module Proof: sig .. end

type t =

`\|`	`Axiom`
`\|`	`Resolved of Reasoner.fact with_proof * Reasoner.clause with_proof`

type 'a with_proof = {

	`conclusion : 'a;`
	`proof : t;`

}

val facts : t -> Reasoner.fact Sequence.t

Iterate on the facts that have been used

val rules : t -> Reasoner.clause Sequence.t

Iterate on the rules that have been used