proposition: Lemma NoDup_filter f l : NoDup l -> NoDup (filter f l).
proof: Proof. induction l as [|a l IHl]; simpl; intros Hnd; auto. apply NoDup_cons_iff in Hnd. destruct (f a); [ | intuition ]. apply NoDup_cons_iff; split; [intro H|]; intuition. apply filter_In in H; intuition. Qed.
imports: PeanoNat