 As an illustration, we can use the Church-Rosser theorem to solve the earlier problem of showing that the two terms \(\bK\) and \(\mathbf{I}\) are not identified by \(\lambda\). The two terms are in \(\beta\)-normal form, so from them there are no \(\beta\)-reduction sequences at all. If \(\bK = \mathbf{I}\) were a theorem of \(\lambda\), then there would be a term \(M\) from which there is a \(\beta\)-reduction path to both \(\mathbf{I}\) and \(\bK\). The Church-Rosser theorem then implies the two paths diverging from \(M\) can be merged. But this is impossible, since \(\bK\) and \(\mathbf{I}\) are distinct \(\beta\)-normal forms.