∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {f : α → β → m β} {init : β} {xs : Array α},
  Array.foldrM f init xs = List.foldlM (fun x y => f y x) init xs.toList.reverse