# Are these 2 lambda calculus terms equivalent?

I have 2 lambda terms and I am not sure whether the rules of bounded variables in the lambda calculus imply that these 2 terms are equivalent or not.

They are:

• $$λc.λc.bc$$
• $$λc.λa.ba$$

I know that in the first of the 2 terms the c's in $$\dots λ \mathbf{c}.b \mathbf{c}$$ are bounded. Likewise the a's in $$\dots \lambda \mathbf{a}.b \mathbf{a}$$ are bounded. But I don't know whether the fact that these are both abstracted on c mean they are equivalent or not.

Yes, $$\lambda c . \lambda c. bc$$ and $$\lambda c . \lambda a.ba$$ are $$\alpha$$-equivalent, i.e. they are equal up to renaming of their bound variables.
Indeed, $$\lambda c. bc$$ and $$\lambda a. ba$$ are $$\alpha$$-equivalent (the latter is just obtained by renaming the bound variable $$c$$ in the former, and vice-versa). And abstraction over a variable that does not occur free ($$c$$ is not free in either $$\lambda c. bc$$ or $$\lambda a. ba$$) preserves $$\alpha$$-equivalence. Therefore, $$\lambda c . \lambda c. bc$$ and $$\lambda c . \lambda a.ba$$ are $$\alpha$$-equivalent.