∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {f : α → β → m β} {init : β} {xs : Array α}
  {a : α},
  Array.foldrM f init (xs.push a) = do
    let init ← f a init
    Array.foldrM f init xs