  Substitution plays a prominent role in the foundation and implementation of
mathematics and computation. In the lambda calculus, we cannot define alpha
congruence without a form of substitution but for substitution and reduction to
work, we need to assume a form of alpha congruence (e.g., when we take lambda
terms modulo bound variables). Students on a lambda calculus course usually
find this confusing. The elegant writings and research of the Curry school have
settled this problem very well. This article is an ode to the contributions of
the Curry school (especially the excellent book of Hindley and Seldin) on the
subject of alpha congruence and substitution.
