Definition of equivalence classes
 A change of bound variables in M is the replacement of a part \x.M by \y.(N[x:=y]) where y does not occur (at all) in N. (Because y is fresh there is no danger in the substitution N[x:=y]).

M is alphacongruent with N, if N results from M by a series of changes of bound variables.