∀ {m : Type u_1 → Type u_2} {α : Type u_1} {i : ℕ} {xs : Array α} {n : ℕ} [inst : Monad m] [LawfulMonad m]
  {f : Fin (n + 1) → m α} (hi : autoParam (i ≤ n) Vector.ofFnM_go_succ._auto_5✝) {h : xs.size = i},
  Vector.ofFnM.go✝ f i ⋯ xs h = do
    let as ← Vector.ofFnM.go✝¹ (fun i => f i.castSucc) i hi xs h
    let a ← f (Fin.last n)
    pure (as.push a)