  Perhaps a concrete example would help. Let us try to prove Cantor’s theorem. The key step in showing there is no surjection \(f : X \to \wp(X)\) by reductio ad absurdum is the construction of the diagonal set \(\{x \in X : x \not\in f(x)\}\).  The proof relies on this object being a set, which it will be a set if “\(x \in X \amp x \not\in f(x) \amp f : X \rightarrow \wp(X)\)” is stratified. This in turn depends on “\(\exists y[y \in \wp(X) \amp \langle y, x\rangle \in f \amp f : X \rightarrow \wp(X)]\)” being stratified. And it isn’t stratified, because “\(\langle y, x\rangle \in f\)” compels ‘\(x\)’ and ‘\(y\)’ to be given the same type, while “\(f : X \rightarrow \wp(X)\)” will compel ‘\(y\)’ to be given a type one higher than ‘\(x\)’. This is because we have subformulæ ‘\(x \in X\)’ and ‘\(y \subseteq X\)’. Notice that we can draw this melancholy conclusion without knowing whether the type of ‘\(f\)’ is one higher than that type of its argument, or two, or three …. We cannot prove Cantor’s theorem.