∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) (x : List β) (a : α)
  (as : List α),
  List.filterMapM.loop f (a :: as) x = do
    let __do_lift ← f a
    match __do_lift with
      | none => List.filterMapM.loop f as x
      | some b => List.filterMapM.loop f as (b :: x)