proposition: Lemma map_mapfilter {A B C} (f:A->option B)(g:B->C) l : map g (mapfilter f l) = mapfilter (fun a => option_map g (f a)) l.
proof: Proof. rewrite map_as_mapfilter, mapfilter_comp. f_equiv. Qed.
imports: Coq(List SetoidList)