proposition: Theorem not_NoDup_hasDup_true : forall (A : Set)(eqd : EqDec A)(ls : list A), (~NoDup ls) -> hasDup eqd ls = true.
proof: Proof. induction ls; intuition idtac; simpl in *. exfalso. eapply H. econstructor. destruct (in_dec (EqDec_dec eqd) a ls). trivial. eapply IHls. intuition idtac. eapply H. econstructor; intuition idtac. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation