proposition: Theorem hasDups_true_not_NoDup : forall (A : Set)(eqd : EqDec A)(ls : list A), hasDups eqd ls = true <-> (~ NoDup ls).
proof: Proof. induction ls; intuition; simpl in *. exfalso. eapply H. econstructor. inversion H2; clear H2; subst. destruct (in_dec (EqDec_dec eqd) a ls); intuition. destruct (in_dec (EqDec_dec eqd) a ls); intuition. eapply H0. intuition. eapply H1. econstructor; intuition. Qed.
imports: FCF.FCF FCF.CompFold ZifyNat