Formalization of simply typed lambda calculus with well scoped deburijn index in Agda.
You can also click here to view the highlighted html version.