proposition: Lemma beval_clause_cons_lit : forall env l cl, beval_clause env (cons_lit l cl) = (beval_lit env l || beval_clause env cl).
proof: Proof. induction cl; simpl. - reflexivity. - destruct (pol a || (negb (pol l))). simpl. btauto. simpl. rewrite IHcl. btauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause