proposition: Theorem removePresent_NoDup : forall (A : Set)(eqd : eq_dec A)(u ls : list A), NoDup ls -> NoDup (removePresent eqd u ls).
proof: Proof. induction ls; intuition; simpl in *. unfold setLet. inversion H; clear H; subst. destruct (in_dec eqd a u); intuition. econstructor; intuition. eapply H2. eapply removePresent_in_only_if. eauto. Qed.
imports: FCF.FCF Permutation