LN: Locally nameless representation with cofinite quantificationThe 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. This approach has been successfully applied to formalize many type syst
