 To prove the theorem, it is sufficient to produce one underivable equation. We have already worked through an example: we used the Church-Rosser theorem to show that the equation \(\bK = \mathbf{I}\) is not a theorem of \(\lambda\). Of course, there’s nothing special about these two terms. A significant generalization of this result is available: if \(M\) and \(N\) in \(\beta\)-normal form but \(M\) is distinct from \(N\), then the equation \(M = N\) is not a theorem of \(\lambda\). (This simple condition for underivability does not generally hold if we add additional rules of inference to \(\lambda\).) 