Confluence by the Z-property for De Bruijn's λ-calculus with nameless dummies, based on PLFA

We present Agda code of a proof of confluence via the Z-property, of the untyped λβ-calculus in De Bruijn's λ-calculus notation with nameless dummies, based on the formalisation of that calculus in the book Programming Language Foundations in Agda.