∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} [inst : Monad m] (f : α → m β) (xs : Vector α n)
  (k : ℕ) (h : k ≤ n) (acc : Vector β k),
  Vector.mapM.go✝ f xs k h acc =
    if h' : k < n then do
      let __do_lift ← f xs[k]
      Vector.mapM.go✝¹ f xs (k + 1) ⋯ (acc.push __do_lift)
    else pure (Vector.cast ⋯ acc)