proposition: Lemma sublist_normalise : forall cl cl', Elim.normalise cl = Some cl' -> sublist cl' cl.
proof: Proof. induction cl. - simpl. intros. inv H; auto. constructor. - simpl; intros. destruct (Elim.normalise cl) eqn:N. + simpl in *. intros. destruct (Elim.get_polarity_rec (var a) c) eqn:POL. * destruct p. destruct (eq_dec (make (negb b) (var a)) a); try discriminate. inv H. specialize (IHcl _ eq_refl). apply SUB_CONS;auto. * inv H. apply SUB_CONS2; auto. + discriminate. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause