If substitution were dropped altogether, then the applicability of detachment would become extremely limited, for instance, \(\textsf{SK}\) no longer would be typable. A compromise between having substitution everywhere and having no substitution at all is to modify the detachment rule so that that includes as much substitution as necessary to ensure the applicability of the detachment rule. Such a rule (without combinatory terms or type assignments) was invented in the 1950s by Carew A. Meredit