 Modern proofs of the Church–Rosser theorem for CL proceed indirectly because one-step reduction fails to have the diamond property. A binary relation \(R\) (e.g., reduction) is said to have the diamond property when \(xRy\) and \(xRz\) imply that \(yRv\) and \(zRv\) for some \(v\). If a binary relation \(R\) has the diamond property, so does its  transitive closure. To exploit this insight in the proof of the  Church–Rosser theorem, a suitable subrelation of reduction has to be found. The sought after subrelation should possess the diamond property, and its reflexive transitive closure should coincide with reduction.