proposition: Lemma beval_cnf_Forall : forall env cls, beval_cnf env cls = true <-> Forall (fun x : clause => beval_clause env x = true) cls.
proof: Proof. induction cls. - simpl; split; auto. - simpl. rewrite andb_true_iff. rewrite IHcls. intuition. inv H1; auto. inv H1; auto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause