proposition: Lemma in_removeDups : forall (ls : list A) a, In a ls -> In a (removeDups ls).
proof: Proof. induction ls; intuition; simpl in *. intuition; subst. destruct (in_dec (EqDec_dec eqd) a0 ls). eauto. simpl. intuition. destruct (in_dec (EqDec_dec eqd) a ls). eauto. simpl. right. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool