proposition: Lemma mapfilter_app {A B} (f:A->option B) l l' : mapfilter f (l++l') = mapfilter f l ++ mapfilter f l'.
proof: Proof. induction l; simpl; auto. destruct f; simpl; auto; f_equal; auto. Qed.
imports: Coq(List SetoidList)