proposition: Lemma xnegate_correct : forall env f, (make_conj (fun x => eval_nformula env x -> False) (xnegate f)) <-> ~ eval_nformula env f.
proof: Proof. intros env f. destruct f as [e o]; destruct o eqn:Op; cbn - [psub]; repeat rewrite eval_pol_sub; fold eval_pol; repeat rewrite eval_pol_Pc; repeat rewrite eval_pol_opp; generalize (eval_pol env e) as x; intro. - tauto. - rewrite eq0_cnf. rewrite (Req_dne sor). tauto. - tauto. - tauto. Qed.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl