∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] (f : α → m (Option β))
  (l : List α) (i : ℕ) (h : i ≤ l.toArray.size),
  Array.findSomeRevM?.find✝ f l.toArray i h = List.findSomeM? f (List.take i l).reverse