See this screenshot of the book "Basic Simple Type Theory". The infinite sequence they refer to is just a way to formalize the concept of having enough variables to work with no matter what. In my case, for practical reasons, all my variables are single unicode chars. I forsee for the next 100 years, that to be plenty of mathematical variables to work with.
So I'm in the process of implementing term substitution and I came across this ambiguity in the book:
What do they mean by the last line? Do they mean the first non-free variable including any bound variables within $(N P)$? Or do they mean the first "open, unused, available" variable in all of $(N P)$ including any abstractors $\lambda w$?
My guess is the latter, since $z$ is a dummy variable and of course this can't interfere with other variable useages.