proposition: Lemma split_polarity_vars : forall p l lp ln lo, Elim.split_polarity p l = (lp,ln,lo) -> ~ is_var_of_cnf p lp /\ ~ is_var_of_cnf p ln /\ ~ is_var_of_cnf p lo.
proof: Proof. induction l ;simpl. - intros. inv H. rewrite is_var_of_cnf_nil. tauto. - intros. destruct (Elim.split_polarity p l) as [[lp' ln'] lo'] eqn:SP. destruct (Elim.normalise a) eqn:NORM. specialize (IHl _ _ _ eq_refl). destruct (Elim.get_polarity_rec p c) eqn:P. destruct p0. inv H. assert (~ is_var_of_clause p l0). { intro. eapply NoDup_no_var in P; auto. eapply normalise_NoDup in NORM ; eauto. } destruct b; rewrite is_var_of_cnf_cons. tauto. tauto. inv H. rewrite is_var_of_cnf_cons. specialize (get_polarity_spec (fun _ => true) p c). rewrite P. tauto. inv H. eapply IHl;eauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause