 Rule \(\boldsymbol{\eta}\) tells us that a certain kind of abstraction is otiose: it is safe to identify \(M\) with the function that, given an argument \(x\), applies \(M\) to \(x\). Through this rule we can also see that all terms are effectively functions. One can intuitively justify this rule using the principle of \(\beta\)-reduction.