Simplify the definition of substitution in Lamdba calculus
Yes, there are several techniques, such as de Bruijn indices and explicit substitutions. Actual implementations, at least those that actually have to work efficiently, use such techniques and never implement substitution by renaming variables.