∀ {m : Type → Type u} [inst : Monad m] {α : Type} (p : α → m Bool) (a : α) (as : List α),
  List.findM? p (a :: as) = do
    let __do_lift ← p a
    match __do_lift with
      | true => pure (some a)
      | false => List.findM? p as