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