proposition: Lemma wf_cons_lit : forall l cl, wf cl -> wf (cons_lit l cl).
proof: Proof. unfold wf. intros. destruct H as (l1 & l2 & EQ). subst. revert l2. induction l1. - simpl. intros. destruct (pol l) eqn:POL. exists nil,(var l::l2). rewrite cons_lit_POS_true by auto. reflexivity. exists (var l::nil),l2. simpl. rewrite cons_lit_POS_false by auto. destruct l ; try discriminate ; reflexivity. - intros. simpl. destruct (pol l) eqn:PL; simpl. destruct (IHl1 l2) as (l1' & l2' & EQ). rewrite EQ. exists (a::l1'), l2'. reflexivity. exists (var l ::a ::l1), l2. destruct l; try discriminate. reflexivity. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause