fact: Definition QTautoChecker (f : BFormula (Formula Q) Tauto.isProp) (w: list QWitness) : bool := @tauto_checker (Formula Q) (NFormula Q) unit qunsat qdeduce (Qnormalise unit) (Qnegate unit) QWitness (fun cl => QWeakChecker (List.map fst cl)) f w.
imports: OrderedRing RingMicromega Refl QArith Qfield EnvRing List Coq.micromega.Tauto