proposition: Lemma get_polarity_spec_not_var : forall p c, ~ is_var_of_clause p c -> Elim.get_polarity_rec p c = None.
proof: Proof. intros. destruct (Elim.get_polarity_rec p c) eqn:G;auto. exfalso. assert (Elim.get_polarity_rec p c <> None) by congruence. apply get_polarity_spec_var in H0. tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause