proposition: Lemma get_polarity_rec_vars_res : forall v v' c b l, Elim.get_polarity_rec v' c = Some (b, l) -> is_var_of_clause v l -> is_var_of_clause v c.
proof: Proof. induction c. - simpl. discriminate. - simpl. intros. destruct (get_pol v' a) eqn:POL. inv H. rewrite is_var_of_clause_cons. tauto. destruct (Elim.get_polarity_rec v' c) eqn: P. destruct p. inv H. rewrite is_var_of_clause_cons in *. intuition. specialize (IHc _ _ eq_refl). tauto. discriminate. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause