proposition: Theorem hasDup_false_NoDup : forall (A : Set)(eqd : EqDec A)(ls : list A), hasDup _ ls = false -> NoDup ls.
proof: Proof. induction ls; intuition idtac; simpl in *. econstructor. destruct (in_dec (EqDec_dec eqd) a ls). discriminate. econstructor; intuition idtac. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation