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