Аннотация. Построены новые доказательства двух теорем бестипового экстенсионального λ-исчисления: теоремы Карри о том, что произвольный λ-терм имеет βη-нормальную форму тогда и только тогда, когда он имеет β-нормальную форму, и теоремы нормализации для βη-редукции. Приведенный подход базируется на двух широко известных результатах: теореме об откладывании η-редукции и свойстве сильной нормализуемости η-редукции, которые позволяют естественным образом распространить некоторые утверждения с обычного λ-исчисления на экстенсиональный случай.

Ключевые слова: бестиповое экстенсиональное λ-исчисление, откладывание η-редукции, теорема о βη-нормальной форме, теорема нормализации для βη-редукции.