module FixpointCertif:sig..end
val useful_instances : Node.t -> Node.t list -> (Node.t * Variable.subst) listReturns the cube instances that were useful in proving the fixpoint. Raises Assertion_failure if it is not a fixpoint. (Useful for certificates)