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 lambdaterm 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.