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

In this paper the polymorphic lambda terms are considered, where no type information is provided for the variables. The aim of this work is to prove that presented typification algorithm [1] typifies such terms in most common way.