Равенство термов

Говорят, что два терма u и v равны, если u = v выводима в лямбда-исчислении:

λ u = v.

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

Понятие '=' не то же самое, что синтаксическая конгруэнтность '≡'! Из u ≡ v следует u = v (рефлексивность), но не наоборот:

λx.x = λy.y ; правило α: λx.x ≡α λy.y
но  λx.x λy.y