proposition: Lemma wf_sublist : forall cl cl' (SUB:sublist cl' cl) (WF: wf cl), wf cl'.
proof: Proof. unfold wf. intros. destruct WF as (n & p & EQ). revert n p EQ. induction SUB;intros. - exists nil. exists nil. reflexivity. - destruct n. destruct p. + discriminate. + inv EQ. destruct (IHSUB nil p eq_refl) as (n1& n2 & EQ). subst. exists n1. exists n2. reflexivity. + inv EQ. destruct (IHSUB _ _ eq_refl) as (n1& n2 & EQ). subst. exists n1. exists n2. reflexivity. - destruct n. destruct p. + discriminate. + inv EQ. destruct (IHSUB nil p eq_refl) as (n1& n2 & EQ). subst. destruct n1. * simpl. exists nil,(h::n2). reflexivity. * simpl in SUB. apply (sublist_forall Lit.isPOS) in SUB. inv SUB. discriminate. rewrite Forall_map. rewrite Forall_forall. intros. reflexivity. + inv EQ. destruct (IHSUB _ _ eq_refl) as (n1& n2 & EQ). subst. exists (h::n1). exists n2. reflexivity. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause