proposition: Lemma QReval_formula_compat : forall env b f, Tauto.hold b (QReval_formula env b f) <-> QReval_formula' env f.
proof: Proof. intros. unfold QReval_formula. destruct f. unfold QReval_formula'. rewrite Reval_op2_hold. apply Reval_pop2_eval_op2. Qed.
imports: OrderedRing QMicromega RingMicromega Refl Sumbool Raxioms Rfunctions RIneq Rpow_def QArith Qfield Qreals DeclConstant EnvRing