alpha-conversion

Lambda terms that differ only in the names of their bound variables will be equated. More precisely, if $y$ is not free in $M$:

$$\lambda x.M =_\alpha \lambda y.M\{X\mapsto y\}$$

Where $M\{x\mapsto y\}$ is the term $M$ where each occurence of $x$ is replaced by $y$, i.e. we rename every free occurrence of $x$ to $y$.

Lambda terms are defined module $\alpha$ conversion, so $\lambda x.x$ and $\lambda y.y$ are the same term. $\alpha$ equivalent terms represent the same computation.