∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → β → β} {b : β}
  {xs : Array α} {start stop : ℕ},
  Array.foldrM (fun x1 x2 => pure (f x1 x2)) b xs start stop = pure (Array.foldr f b xs start stop)