 for \(\phi\) of “any” type. (Note that this differs from ∗13·01 in that the shriek no longer appears.) Now to prove this, assume both ∗13·01 and the Axiom of Reducibility, and suppose, for proof by reductio, that \(x = y\), and \(\phi x\), and not \(\phi y\), for some function \(\phi\) of arbitrary type. Then, the Axiom of Reducibility ∗12·1 guarantees that there will be a predicative function \(\psi \bang\), which is coextensive with \(\phi\) such that \(\psi \bang x\) but not \(\psi \bang y\), which contradicts ∗13·01.