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

In this paper polymorphic lambda terms are considered, where no type information is provided for the variables. The aim of this work is to extend the algorithm of typification [1] of such terms introducing type constants and term constants.