proposition: Lemma cons_lit_NEG_wf : forall v l1 l2, (cons_lit (NEG v) (map NEG l1 ++ map POS l2)) = map NEG (v::l1) ++ (map POS l2).
proof: Proof. destruct l1;simpl;auto. destruct l2;simpl;auto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause