∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] {f : β → α → m β} {xs : Array α} {i j : ℕ},
  xs.size ≤ i + j → ∀ {b : β}, Array.foldlM.loop f xs xs.size ⋯ i j b = List.foldlM f b (List.drop j xs.toList)