 In pure typefree CL, an expression of the form \(MM\) is a well-formed term.  Moreover, terms of this form can enter into provable equations and inequations in multiple ways. For example, \(xx=xx\) is an axiom, and by one of the rules, \(y(xx)=y(xx)\) is provable too. A more interesting occurrence of a term of the form \(MM\) can be seen in the provable inequation \(\textsf{S} (\textsf{SKK})(\textsf{SKK})x\triangleright xx\).