Даже если понимать под типизацией не определение principle type (наиболее общего типа), а указание какого-то из допустимых, то


Проблема всегда в том, что значит "имеет тип". Если тип неявен и выводится из структуры терма по определенным правилам - это типизация по Карри, в этом случае данный артефакт имеется. А при типизации по Черчу, где каждый подтерм изучаемого терма явно типизирован (тип явно приписан любому терму), всё OK и есть лемма уникальности типов.