proposition: Lemma beval_cnf_cons_lit : forall env l lp, beval_cnf env (map (cons_lit l) lp) = (Lit.beval_lit env l || (beval_cnf env lp)).
proof: Proof. induction lp;simpl. - btauto. - rewrite IHlp. rewrite beval_clause_cons_lit. btauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause