proposition: Lemma split_polarity_vars_spec : forall v' v cls lp ln lo, Elim.split_polarity v' cls = (lp, ln, lo) -> is_var_of_cnf v (lp++ln++lo) -> is_var_of_cnf v cls /\ v <> v'.
proof: Proof. split. - revert lp ln lo H H0. induction cls. + simpl. intros. inv H. rewrite is_var_of_cnf_nil in H0. tauto. + intros. simpl in H. destruct (Elim.split_polarity v' cls) as ((lp',ln'),lo'). specialize (IHcls _ _ _ eq_refl). destruct (Elim.normalise a) eqn:N. apply normalise_vars with (p:= v) in N. destruct (Elim.get_polarity_rec v' c) eqn:GP. destruct p. inv H. rewrite! is_var_of_cnf_app in H0. rewrite is_var_of_cnf_cons. specialize (get_polarity_rec_vars_res v _ _ _ _ GP). rewrite! is_var_of_cnf_app in *. destruct b; rewrite !is_var_of_cnf_cons in *. tauto. tauto. inv H. rewrite is_var_of_cnf_cons. rewrite! is_var_of_cnf_app in *. rewrite is_var_of_cnf_cons in *. tauto. rewrite is_var_of_cnf_cons. rewrite! is_var_of_cnf_app in *. inv H. tauto. - apply split_polarity_vars in H. rewrite! is_var_of_cnf_app in H0. intuition congruence. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause