∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Vector α n}
  {f : (i : ℕ) → α → i < n → m β}, Vector.toArray <$> xs.mapFinIdxM f = xs.toArray.mapFinIdxM fun i x h => f i x ⋯