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 alpha-congruent with N, if N results from M by a series of changes of bound variables.