Изменения

Согласимся '''первым символом''' <tex>t</tex> называть <tex>x</tex> в первом случае, и <tex>\Pi</tex> во втором. '''Первыми переменными''' <tex>t</tex> будем называть переменные <tex>x_1, \ldots, x_n</tex>.}}

{{Определение|definition=Терм <tex>t</tex> типа <tex>T</tex> в контексте <tex>G</tex> называется '''объектом''' в <tex>\Gamma</tex>, если <tex>\Gamma \vdash T : \mathrm{Type}</tex>}}

{{Утверждение|statement=Задача вывода типов в пустом контексте разрешима в <tex>\lambda\Pi</tex>-исчислении.|proof=Типизируемые в пустом контексте чистые термы <tex>\lambda\Pi</tex> исчисления совпадают с типизируемыми выражениями просто типизированного <tex>\lambda</tex>-исчисления, а задача вывода типов в просто типизированном <tex>\lambda</tex>-исчислении разрешима.}}