proposition: Lemma cons_lit_POS_false : forall l cl, pol l = false -> cons_lit l cl = l :: cl.
proof: Proof. induction cl;simpl. - reflexivity. - intros. rewrite H. rewrite orb_comm. simpl. reflexivity. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause