 The calculi \(\text{CL}_\triangleright\) and \(\text{CL}_=\) of the previous section formalize reduction and equality. However, \(\triangleright\) and \(=\)  have some further properties that are important when the terms are thought to stand for functions.  The next theorem is one of the earliest and best-known results about CL.