Индукцией по генерации M вроде даказывается.
Я ж выше привел пример, когда это просто неверно.

Не предполагая этого правила ("в контекст можно добавлять "свежую" для этого контекста переменную"), тип (\x:a.\x:b.x) вывести нельзя.

Поэтому это правило надо формально добавить в набор правил типизации.