Actually, we are mostly interested in equivalence classes

• Identify two terms if each can be transformed to the other by a renaming of its bound variables.
• Consider a lambda-term as a representative of its equivalence class.
• Interpret substitution, M[x:=N] , as an operation on the equivalence classes of M and N. This operation can be performed using representatives, provided that the bound variables are named properly. i.e. as far apart as possible.