proposition: Lemma RWeakChecker_sound : forall (l : list (NFormula Q)) (cm : RWitness), RWeakChecker l cm = true -> forall env, make_impl (Qeval_nformula env) l False.
proof: Proof. intros l cm H. intro. unfold Qeval_nformula. apply (checker_nf_sound Rsor QSORaddon l cm). unfold RWeakChecker in H. exact H. Qed.
imports: OrderedRing QMicromega RingMicromega Refl Sumbool Raxioms Rfunctions RIneq Rpow_def QArith Qfield Qreals DeclConstant EnvRing List