proposition: Lemma filter_as_mapfilter {A} (f:A->bool) l : filter f l = mapfilter (fun a => if f a then Some a else None) l.
proof: Proof. induction l; simpl; auto. destruct f; simpl; auto. f_equal; auto. Qed.
imports: Coq(List SetoidList)