proposition: Lemma cons_lit_POS_wf : forall v l1 l2, (cons_lit (POS v) (map NEG l1 ++ map POS l2)) = map NEG l1 ++ (map POS (v::l2)).
proof: Proof. induction l1;simpl. - destruct l2 ; reflexivity. - intros. f_equal. rewrite IHl1. reflexivity. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause