proposition: Lemma mapfilter_comp {A B C}(f:A->option B)(g:B->option C) l : mapfilter g (mapfilter f l) = mapfilter (fun a => option_bind (f a) g) l.
proof: Proof. induction l; simpl; auto. destruct f; simpl; auto. destruct g; simpl; auto. f_equal; auto. Qed.
imports: Coq(List SetoidList)