 The Church-Rosser theorem gives us, among other things, that the plain \(\lambda\)-calculus—that is, the theory \(\lambda\) of equations between \(\lambda\)-terms—is consistent, in the sense that not all equations are derivable.