Об исчислении Ламбека с одним делением и одним примитивным типом, допускающем пустые антецеденты

Доказывается следующее утверждение: правило вывода, заданное схемой, допустимо в исчислении Ламбека с одним делением $\mathrm{L}^*(\backslash)$, допускающем пустые антецеденты, тогда и только тогда, когда оно допустимо во фрагменте $\mathrm{L}^*(\backslash)$ с одним примитивным типом $\mathrm{L}^*(\backslash; p_1)$. Для этого применяется подстановка типов, сводящая выводимость в $\mathrm{L}^*(\backslash)$ к выводимости в $\mathrm{L}^*(\backslash;p_1)$.