proposition: Lemma cons_lit_POS_true : forall l cl, pol l = true -> cons_lit l (map POS cl) = POS (var l) :: map POS cl.
proof: Proof. induction cl. - simpl. intros. destruct l; simpl ; auto. discriminate. - intros. simpl. destruct l; simpl ; auto. discriminate. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause