  We present a short proof of the Church-Rosser property for the
lambda-calculus enjoying two distinguishing features: Firstly, it employs the
Z-property, resulting in a short and elegant proof; and secondly, it is
formalized in the nominal higher-order logic available for the proof assistant
Isabelle/HOL.

Logic in Computer Science