proposition: Lemma NoDup_no_var : forall p c (ND : NoDup (vars_of_clause c)) b c', Elim.get_polarity_rec p c = Some (b, c') -> is_var_of_clause p c' -> False.
proof: Proof. induction c. - intros. simpl in H. discriminate. - intros. simpl in ND. inv ND. simpl in H. destruct (get_pol p a) eqn:POL. + inv H. apply get_pol_inv in POL. subst. rewrite Lit.var_make in H3. rewrite <- vars_of_clause_ok in H3. tauto. + apply get_pol_None in POL. destruct (Elim.get_polarity_rec p c) eqn:GP; try discriminate. destruct p0. inv H. rewrite is_var_of_clause_cons in H0. destruct H0; try tauto. eapply IHc;eauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause