proposition: Lemma beval_cnf_exists : forall env cls, (beval_cnf env cls = true -> False) -> exists cl, In cl cls /\ beval_clause env cl = false.
proof: Proof. induction cls;simpl. - tauto. - intros. rewrite andb_true_iff in H. destruct (beval_clause env a) eqn:EC. specialize (fun E => H (conj eq_refl E)). apply IHcls in H. destruct H as (c & T1 & T2). exists c. tauto. exists a. tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause