proposition: Lemma get_polarity_rec_sublist : forall p cl b cl', Elim.get_polarity_rec p cl = Some(b,cl') -> sublist cl' cl /\ In (make b p) cl.
proof: Proof. induction cl. - simpl. discriminate. - simpl. intros. destruct (get_pol p a) eqn:GP. inv H. apply get_pol_inv in GP. split ; intuition. constructor. apply sublist_refl. destruct (Elim.get_polarity_rec p cl) eqn: GP'. destruct p0. inv H. apply get_pol_None in GP. specialize (IHcl _ _ eq_refl). intuition. apply SUB_CONS2. auto. discriminate. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause