The combinatory rules in B&K-CCG, given in Figure 4, are defined to be sensitive to the slash types.
consider the following instance of forward harmonic composition: This rule should be understood as obtaining its conclusion a=c from the primary premise a=b by the removal of the argument =b and the subsequent transfer of the argument =c from the secondary premise.