In this episode, I discuss the paper Nominal Techniques in Isabelle/HOL, by Christian Urban.  This paper shows how to reason with terms modulo alpha-equivalence, using ideas from nominal logic.  The basic idea is that instead of renamings, one works with permutations of names.