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.