 One can view rule \(\mathbf{Ext}\) as a kind of generalization principle. If we have derived that \(Mx = Nx\), but \(x\) figures in neither \(M\) nor \(N\), then we have effectively shown that \(M\) and \(N\) are alike. Compare this principle to the principle of universal generalization in first-order logic: if we have derived \(\phi(x)\) from a set \(\Gamma\) of hypotheses in which \(x\) is not free, then we can conclude that \(\Gamma\) derives \(\forall x\phi\).