∀ {α : Type u_1} {β : Type u_2} {start start' stop stop' : ℕ} {m : Type u_2 → Type u_3} [inst : Monad m]
  {f g : α → β → m β} {b : β} {xs xs' : Array α},
  xs = xs' →
    (∀ (x : α) (y : β), f x y = g x y) →
      start = start' → stop = stop' → Array.foldrM f b xs start stop = Array.foldrM g b xs' start' stop'