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