proposition: Lemma NoDup_filter A (l: list A) (ND: NoDup l) f : NoDup (filter f l).
proof: Proof. induction l; intros; try constructor. simpl. destruct (f a) eqn:?; simpl; inversion ND; subst; auto. apply NoDup_cons; auto. rewrite In_filter. tauto. Qed.
imports: Coq(List Permutation)