proposition: Theorem removeDups_NoDup : forall (ls : list A), NoDup (removeDups ls).
proof: Proof. induction ls; intuition; simpl in *. econstructor. destruct (in_dec (EqDec_dec eqd) a ls); intuition. econstructor; intuition. eapply n. eapply removeDups_in. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool