proposition: Lemma Qeval_nformula_dec : forall env d, (Qeval_nformula env d) \/ ~ (Qeval_nformula env d).
proof: Proof. exact (fun env d =>eval_nformula_dec Qsor (fun x => x) env d). Qed.
imports: OrderedRing RingMicromega Refl QArith Qfield EnvRing