proposition: Lemma Reval_formula_compat : forall env b f, Tauto.hold b (Reval_formula env b f) <-> Reval_formula' env f.
proof: Proof. intros. unfold Reval_formula. destruct f. unfold Reval_formula'. simpl. 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