 The rule \(\boldsymbol{\omega}\) has infinitely many hypotheses: on the assumption that \(Mx = Nx\), no matter what \(x\) may be, then we can conclude that \(M = N\). The \(\boldsymbol{\omega}\) rule is an analogue in the \(\lambda\)-calculus of the rule of inference under the same name in formal number theory, according to which one can conclude the universal formula \(\forall x\phi\) provided one has proofs for \(\phi(x := \mathbf{0}), \phi(x := \mathbf{1}),\ldots\) . Note that unlike the rule \(\mathbf{Ext}\), the condition that \(x\) not occur freely in \(M\) or \(N\) does not arise.