proposition: Lemma get_polarity_spec_var : forall p c, Elim.get_polarity_rec p c <> None -> is_var_of_clause p c.
proof: Proof. induction c ; simpl. - rewrite is_var_of_clause_nil. tauto. - destruct (get_pol p a) eqn: POL. rewrite is_var_of_clause_cons. intros. apply get_pol_inv in POL. subst. rewrite var_make. tauto. destruct (Elim.get_polarity_rec p c); try congruence. destruct p0. intros. apply get_pol_None in POL. rewrite is_var_of_clause_cons. intuition congruence. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause