proposition: Lemma eval_clauses_all_pos : forall env p cl cls (INC : In cl cls) (ALLP : forall l : t, In l cl -> l = POS p), eval_cnf env cls -> env p.
proof: Proof. induction cls. - simpl. tauto. - intros. simpl in H. destruct H. destruct INC. subst. eapply eval_clause_POS in ALLP; eauto. eapply IHcls; eauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause