proposition: Lemma filter_map {A B} (f:A->B)(h:B->bool) l : filter h (map f l) = map f (filter (fun x => h (f x)) l).
proof: Proof. induction l; simpl; auto. destruct (h (f a)); simpl; f_equal; auto. Qed.
imports: Coq(List SetoidList)