proposition: Lemma list_filter_ok f (m:list key) : NoDupA K.eq m -> NoDupA K.eq (List.filter f m).
proof: Proof. induction 1; simpl. - constructor. - destruct (f x); trivial. constructor; trivial. contradict H. rewrite InA_alt in *. destruct H as (y,(Hy,H)). exists y; split; trivial. now rewrite filter_In in H. Qed.
imports: Coq(EqualitiesFacts)