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