proposition: Lemma eval_cnf_cons_iff : forall env a f, ((~ make_conj (eval_tt env) a) /\ eval_cnf env f) <-> eval_cnf env (a::f).
proof: Proof. Proof using. intros; clear. unfold eval_cnf in *. rewrite make_conj_cons ; eauto. unfold eval_clause. tauto. Qed.
imports: List Refl Bool Relation_Definitions Setoid