proposition: Lemma Qeval_formula_compat : forall env b f, Tauto.hold b (Qeval_formula env b f) <-> Qeval_formula' env f.
proof: Proof. intros. unfold Qeval_formula. destruct f. repeat rewrite Qeval_expr_compat. unfold Qeval_formula'. unfold Qeval_expr'. simpl. rewrite Qeval_op2_hold. split ; destruct Fop ; simpl; auto. Qed.
imports: OrderedRing RingMicromega Refl QArith Qfield EnvRing