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