Someone suggested to me that the halting problem could be solved by a lambda calculus "program", which reduces to $\lambda y.y$ if an input program halts and $\lambda n.n$ if it does not. Therefore it is not possible to extend this into a program that halts if it thinks it doesn't halt. (That's just background, not the question proper)
I said this is nonsense, because obviously these are the same term written differently. He says we can just look at the output and see whether the variable is called $y$ or $n$, even though a lambda calculus program can't.
I think the lambda calculus reduction rules allow any variable to be renamed at any time for no reason whatsoever, so we can't reliably say what variables will be called after reducing a lambda calculus expression.
Are $\lambda y.y$ and $\lambda n.n$ considered "the same" or equal in lambda calculus?