On strong normalization and type inference in the intersection type discipline