Теории λ+ext и λη

λ+ext u x = v x ⇒ u = v
где x ∉ FV(u) ∪ FV(v),
т.е. x не является свободной ни в u, ни в v.		 (правило ext)
λη u →η v ⇒ u = v
где λx.(v x) →η v
и x ∉ FV(v),
т.е. x не является свободной в v.		 (правило η)
(η-конверсия)

Добавление дополнительного правила η к теории λ даёт расширенные теории, в которых можно вывести больше формул (равенств).

Иногда отношение =βη в этой теории называют βη-эквивалентностью термов.

Пример
λx.y x →η y ; x не входит в оператор y
но λx.(x x) η x ; x является свободной в операторе тела (x x)