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