proposition: Lemma wf_cons : forall l cl, wf (l :: cl) -> if pol l then Forall (fun l => pol l = true) cl else wf cl.
proof: Proof. intros. unfold wf in H. destruct H as (l1 & l2 & EQ); subst. destruct l1. simpl in EQ. destruct l; simpl;auto. destruct l2. inv EQ. inv EQ. rewrite Forall_map. rewrite Forall_forall. reflexivity. destruct l2 ; discriminate. inv EQ. simpl. exists l1,l2;auto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause