proposition: Lemma wf_cons_sublist : forall a cl c, wf (a :: cl) -> sublist c cl -> wf (a :: c).
proof: Proof. intros. apply wf_cons in H. destruct (pol a) eqn:PA. - unfold wf. exists nil, (map var (a::c)). simpl. f_equal. destruct a; try discriminate;auto. rewrite map_map. apply sublist_forall with (P:= Lit.isPOS) in H0; auto. induction H0 ; simpl. reflexivity. destruct x ; try discriminate. f_equal. auto. - apply wf_sublist in H0;auto. unfold wf in H0. destruct H0 as (l1&l2& EQ). subst. destruct a; try discriminate. exists (f::l1),l2. reflexivity. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause