proposition: Lemma is_var_of_cnf_elim : forall v v' cls, is_var_of_cnf v (Elim.elim v' cls) -> (is_var_of_cnf v cls /\ v <> v').
proof: Proof. unfold Elim.elim. intros. destruct (Elim.split_polarity v' cls) as ((lp,ln),lo) eqn:E. apply split_polarity_vars_spec with (v:=v) in E;auto. rewrite is_var_of_cnf_app in H. rewrite! is_var_of_cnf_app. intuition. apply is_var_of_cnf_resolve in H0. rewrite! is_var_of_cnf_app in H0. tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause