proposition: Lemma eval_clause_cons_lit_POS : forall env l cl, Forall (fun l : t => pol l = true) cl -> eval_lit env l (eval_clause env cl) <-> eval_clause env (cons_lit l cl).
proof: Proof. intros. induction H. - simpl. tauto. - simpl. rewrite H. simpl. tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause