How do you deal with variable binders when mechanizing metatheory?
I'm a brainlet who can't into nominal sets or parametric higher order abstract syntax.
They just seem really clumsy compared to using simple capture avoiding substitution of strings.
The less said about de Bruijn indices the better.