proposition: Lemma cnf_of_list_correct : forall (T : Type) env l tg, eval_cnf (Annot:=T) eval_nformula env (cnf_of_list l tg) <-> make_conj (fun x : NFormula => eval_nformula env x -> False) l.
proof: Proof. unfold cnf_of_list. intros T env l tg. set (F := (fun (x : NFormula) (acc : list (list (NFormula * T))) => if check_inconsistent x then acc else ((x, tg) :: nil) :: acc)). set (G := ((fun x : NFormula => eval_nformula env x -> False))). induction l as [|a l IHl]. - compute. tauto. - rewrite make_conj_cons. simpl. unfold F at 1. destruct (check_inconsistent a) eqn:EQ. + rewrite IHl. unfold G. destruct a. specialize (check_inconsistent_sound _ _ EQ env). simpl. tauto. + rewrite <- eval_cnf_cons_iff. simpl. unfold eval_tt. simpl. rewrite IHl. unfold G at 2. tauto. Qed.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl