fact: Fixpoint filter_map `(f : a -> option b) (x : t a) : t b := Seq (fun _ => match unseq x with | Cons x rst => match f x with | Some y => Cons y (filter_map f rst) | _ => unseq (filter_map f rst) end | Nil => Nil end).
imports: Coq(Extraction)