proposition: Lemma beval_clauses_Nil : forall p, (forall env : HFormula -> bool, beval_cnf env nil = true -> env p = true) -> False.
proof: Proof. intros. simpl in H. specialize (H (fun _ => false) eq_refl). discriminate. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause