proposition: Lemma cnf_negate_correct : forall (T : Type) env t (tg:T), eval_cnf eval_nformula env (cnf_negate t tg) <-> ~ eval_formula env t.
proof: Proof. intros T env t tg. rewrite normalise_sound. unfold cnf_negate. generalize (normalise t) as f;intro f. destruct (check_inconsistent f) eqn:U. - destruct f as [e o]. assert (US := check_inconsistent_sound _ _ U env). rewrite eval_cnf_tt. tauto. - rewrite cnf_of_list_correct. apply xnegate_correct. Qed.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl