proposition: Lemma NoDup_dec {A : Type} : forall (l : list A), (forall x y : A, {x = y} + {x <> y}) -> NoDup l \/ ~ NoDup l.
proof: Proof. intros l HDec. induction l. left. apply NoDup_nil. elim IHl; clear IHl; intro H. assert (HIn := in_dec HDec a l). elim HIn; clear HIn; intro HIn. right. clear H. intro H. assert (H' := NoDup_remove_2 nil l a). simpl in H'. apply H' in H. contradiction. left. apply NoDup_cons; assumption. right. intro H'. apply H. clear H. assert (H := NoDup_remove_1 nil l a). simpl in H. auto. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality