 For any formula \(\phi\), define \(\phi^+\) as the formula obtained by raising every type index on a variable in \(\phi\) by one. Quine observes that any proof of \(\phi\) can be converted into a proof of \(\phi^+\) by raising all type indices in the original proof. Further, every object \(\{x^n \mid \phi \}^{n+1}\) that the theory permits us to define has a precise analogue \(\{x^{n+1} \mid \phi^{+}\}^{n+2}\) in the next higher type; this can be iterated to produce “copies” of any defined object in each higher type.