 Theorem. \(A\rightarrow B\) is a theorem of the intuitionistic implicational logic, denoted by \(IPC_\rightarrow\) or \(J_\rightarrow\), iff for some \(M\), \(M\colon A\rightarrow B\) is a provable type assignment in TA\(_\textrm{CL}\), where the term \(M\) is built from \(\textsf{S}\) and \(\textsf{K}\), that is, \(M\) is a combinator over the base \(\{\textsf{S},\textsf{K}\}\). 