 The rule of substitution is built-in into the formulation of \(\textrm{TA}_\textrm{CL}\) via the rule schema called detachment and the axiom schemas for the basic combinators. It is obvious that there are formulas of least complexity that are types of \(\textsf{S}\) and \(\textsf{K}\), such that all the other types of \(\textsf{S}\) and \(\textsf{K}\) are their substitution instances. A formula that has this property is called a principal type of a combinator. Obviously, a combinator that has a principal type, has denumerably many principal types, which are all substitution instances of each other; hence, it is justified to talk about the principal type schema of a combinator. The existence of principal types for complex combinators is not obvious, nevertheless, obtains.