proposition: Lemma normalise_NoDup : forall a c, Elim.normalise a = Some c -> NoDup (vars_of_clause c).
proof: Proof. induction a. - simpl. intros. inv H. constructor. - simpl. intros. destruct (Elim.normalise a0) eqn:N. destruct (Elim.get_polarity_rec (var a) c0) eqn:GP. destruct p. destruct (eq_dec (make (negb b) (var a)) a). + discriminate. + inv H. apply IHa; auto. + inv H. simpl. constructor. generalize (get_polarity_spec (fun _ => true) (var a) c0). rewrite GP. rewrite vars_of_clause_ok. auto. apply IHa;auto. + discriminate. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause