> Even moreso if variable names are replaced by De Bruijn indices. De Bruijn indices are not simply variable names: they vary dynamically depending where in th

> Even moreso if variable names are replaced by De Bruijn indices. De Bruijn indices are not simply variable names: they vary dynamically depending where in the term (i.e. under how many binders) they occur, which is why beta reduction is so hairy with the De Bruijn notation.