∀ {α : Type u} {β : Type v} (f : α → Option β) (x : List α),
  List.filterMap f x =
    match x with
    | [] => []
    | a :: as =>
      match f a with
      | none => List.filterMap f as
      | some b => b :: List.filterMap f as