The Informal Description section on Wikipedia is good for more background on Lambda Calculus:
It works, but it's very fiddly. My favourite way of solving the problem of names in the lambda calculus is to use Pitts-Gabbay nominal syntax. Wikipedia has a weak article on them, which I mean someday to fix up: https://en.wikipedia.org/wiki/Nominal_terms_(computer_scienc...
https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.36...