fact: Definition eval_formula (env : PolEnv) (f : Formula C) : Prop := let (lhs, op, rhs) := f in (eval_op2 op) (eval_pexpr env lhs) (eval_pexpr env rhs).
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl