Church-Rosser theorem (source code)

= Church-Rosser theorem
{c}
{wiki}

If a lambda term beta-reduces to both $M$ and $N$, then $M$ and $N$ beta-reduce to a common term. Consequently two beta-equivalent beta-normal forms are alpha-equivalent.