 Alpha equivalence

Two lambda terms are alpha-equivalent when they differ only by consistent renaming of bound variables.