proposition: Theorem hasDups_false_NoDup : forall (A : Set)(eqd : EqDec A)(ls : list A), hasDups _ ls = false <-> NoDup ls.
proof: Proof. induction ls; intuition; simpl in *. econstructor. destruct (in_dec (EqDec_dec eqd) a ls). discriminate. econstructor; intuition. inversion H1; clear H1; subst. destruct (in_dec (EqDec_dec eqd) a ls); intuition. Qed.
imports: FCF.FCF FCF.CompFold ZifyNat