Сохранение эквивалентности выводов при редукции глубины формул

В работе рассматриваются выводы в $(\&\supset)$ – фрагменте интуиционистского исчисления высказываний.
Как известно, замена любого вхождения формулы $\Phi[F]$ в секвенцию $S$ на вхождение формулы $\Phi[p]$, где $p$ – новая пропозициональная переменная, с одновременным добавлением в антецедент формулы $F\supset p$ или $p\supset F$ в зависимости от знака вхождения $F$ в $S$, оставляет выводимость неизменной.
Приводится доказательство того, что естественное продолжение этого преобразования на выводы сохраняет отношение эквивалентности выводов, т.е. преобразованные выводы эквивалентны тогда и только тогда, когда эквивалентны исходные. (Выводы считаются эквивалентными, если совпадают некоторые их нормальные формы или, что то же, эквивалентны их дедуктивные термы.)
Показано, что итерацией этого преобразования каждый вывод произвольной секвенции $S$ может быть преобразован в вывод секвенции $S'$, зависящей только от $S$, сукцедент которой – переменная, а в антецедент входят только формулы вида $a$, $a\&b$, $a\supset b$, $(a\supset b)\supset c$, $a\&b\supset c$, $a\supset(b\&c)$, где $a,b,c$ – переменные. При этом, если $S$ уравновешена, то $S'$ тоже уравновешена. (Секвенция называется уравновешенной, если каждая переменная входит в нее не более двух раз).
Известное соответствие между некоторыми понятиями теории категорий и понятиями теории доказательств позволяет утверждать, что построен унивалентный функтор, отображающий свободную декартово замкнутую категорию в себя. Библ. – 5 назв.