confluence of reduction, the correctness of types, the
uniqueness of types up to conversion, the subject reduction of the type
assignment, the strong normalization of the typed terms. The
confluence of reduction, the correctness of types, the
uniqueness of types up to conversion, the subject reduction of the type
assignment, the strong normalization of the typed terms. The