[Time skip]
Кому интересно, я потом от этого стремления ушёл. Мне нужно было просто записывать натуральную дедукцию более скромно, линейно, а это можно устроить, используя старых добрых Карри—Говарда, собирая выводы некой штуки в соответствующий тип и конкретным выводам сопоставляя терм-значение, а выводам из гипотез

— термы вида

, ну и т. д., получается какая-нибудь теория типов. Гипотетические выводы в посылках меня только и путали.