nLab
Church-Rosser theorem

Idea

The Church–Rosser theorem states that the reduction rule?s of the lambda calculus are confluent.