 The Church-Rosser theorem implies the existence of \(\beta\)-reduction sequences commencing from \(\bK\) and from \(\mathbf{I}\) that end at a common term. But there are no \(\beta\)-reduction sequences at all commencing from \(\mathbf{I}\), because it is in \(\beta\)-normal form, and likewise for \(\bK\).