 Roughly, we need to adhere to the principle that free variables ought to remain free; when an occurrence of a variable is threatened to become bound by a substitution, simply perform enough \(\alpha\)-conversions to sidestep the problem. If we keep this in mind, we can work with \(\lambda\)-calculus without worrying about these nettlesome syntactic difficulties.  So, for example, we can't apply the function \(\lambda x[\lambda y[x(y-5)]]\) to the argument \(2y\) because upon substitution of “\(2y\)” for “\(x\)”, the “\(y\)” in “\(2y\)” would be captured by the variable-binding operator “\(\lambda y\)”.  Such a substitution would yield a function different from the one intended. However, we can first transform \(\lambda x[\lambda y[x(y-5)]]\) to \(\lambda x[\lambda z[x(z-5)]]\) by \(\alpha\)-conversion, and then apply this latter function to the argument \(2y\).  So whereas the following is not a valid use of \(\beta\)-conversion:     \[ (\lambda x[\lambda y[x(y-5)]])2y  \rhd \lambda y[2y(y-5)]\]  we can validly use \(\beta\)-conversion to conclude:     \[ (\lambda x[\lambda z[x(z-5)]])2y \rhd \lambda z[2y(z-5)]\]  This example helps one to see why the proviso to \(\beta\)-conversion is so important.  The proviso is really no different from the one used in the statement of an axiom of the predicate calculus, namely: \(\forall x\phi \to \phi^{\tau}_x\), provided no variable that is free in the term \(\tau\) before the substitution becomes bound after the substitution.