The locally nameless representation with cofinite quantification is a pratical technique for representing binders in a formal settings. The locally nameless representation avoids the need for alpha-conversion and the need for shifting de Bruijn indices. The cofinite quantification is used to obtain strong induction principles. On this page, you willl find a collection of examples formalized in Coq using this approach.

Details on tactics and automation techniques used above can be found here.

I maintain a non-exhaustive list of users.