 \(\text{CL}_\triangleright\) and \(\text{CL}_=\) share a feature that may or may not be desirable—depending on what sort of understanding of functions is to be captured. To illustrate the issue, let us consider the one-place combinators \(\textsf{SKK}\) and \(\textsf{SK}(\textsf{KK})\). It is easy to verify that \(\textsf{SKK}M\triangleright M\) and \(\textsf{SK}(\textsf{KK})M \triangleright M\). However, neither \(\textsf{SKK}\triangleright \textsf{SK}(\textsf{KK})\) nor \(\textsf{SK}(\textsf{KK})\triangleright \textsf{SKK}\) is provable in \(\text{CL}_\triangleright\); a fortiori, the equality of the two terms in not provable in \(\text{CL}_=\). This means that  \(\text{CL}_\triangleright\) and \(\text{CL}_=\) formalize intensional notions of functions, where “intensionality” implies that functions that give the same output on the same input may remain distinguishable.