proposition: Theorem hasDup_true_not_NoDup : forall (A : Set)(eqd : EqDec A)(ls : list A), hasDup eqd ls = true -> NoDup ls -> False.
proof: Proof. induction ls; intuition idtac; simpl in *. discriminate. destruct (in_dec (EqDec_dec eqd) a ls). inversion H0; clear H0; subst. intuition idtac. inversion H0; clear H0; subst. intuition idtac. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation