On the type correctness of polymorphic $\lambda$-terms. 2

В работе рассматриваются полиморфные $\lambda$-термы, в которых отсутствует информация о типах переменных. Цель даной работы – доказать, что представленный в [1] алгоритм типизации выводит самый общий тип таких термов.