 This type assignment system is equivalent to the intersection type assignment system for the \(\lambda\)-calculus, and it allows a more precise characterization of classes of terms with respect to the termination of reduction sequences.