proposition: Lemma neg_concl : forall cls l, (forall env, beval_cnf env cls = true -> boeval env l = true) <-> (forall env, beval_cnf env (clause_of_opt l ++ cls) = true -> False).
proof: Proof. split;intros. rewrite beval_cnf_app in *. rewrite andb_true_iff in H0. destruct H0. apply H in H1. rewrite eval_clause_of_opt in H0. rewrite H1 in H0. discriminate. specialize (H env). rewrite beval_cnf_app in H. rewrite eval_clause_of_opt in H. destruct (boeval env l); auto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause