proposition: Lemma NoDupA_filter {A} (eq:relation A) (f:A->bool) l : NoDupA eq l -> NoDupA eq (filter f l).
proof: Proof. induction 1; simpl; auto. destruct f; auto. constructor; auto. rewrite InA_alt in *. setoid_rewrite filter_In. firstorder. Qed.
imports: Coq(List SetoidList)