 It is also not too hard to show that if all typed versions of a generalized positive formula \(\phi\) in the language of the intended model (with sequences \(s\) appearing as values of free variables replaced by their values at the appropriate types) are true, then the original formula \(\phi\) is true in the intended model. The one difficulty comes in with existential quantification: the fact that one has a witness to \((\exists x.\phi(x))\) in each typed version does not immediately give a sequence witnessing this in the intended model. The tree property of \(\omega\) helps here: only finitely many approximants to sets exist at each level, so one can at each level choose an approximant refinements of which are used at infinitely many higher levels as witnesses to \((\exists x.\phi(x))\), then restrict attention to refinements of that approximant; in this way one gets not an arbitrary sequence of witnesses at various types but a “convergent” sequence (an element of the intended model).