 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. Meredith, and it is usually called condensed detachment. The key to the applicability of detachment is to find a common substitution instance of the minor premise and of the antecedent of the major premise. This step is called unification.  (A bit more formally, let \(s(A)\) denote the application of the substitution \(s\) to \(A\).  Then, the result of the condensed detachment of \(A\) from \(B\rightarrow C\) is \(s(C)\), when there is an \(s\) such that \(s(A)= s(B)\), and for any \(s_1\) with this property, there is an \(s_2\) such that \(s_1\) is the composition of \(s\) and \(s_2\).)