 Definition (change of bound variables, \(\alpha\)-convertibility). The term \(N\) is obtained from the term \(M\) by a change of bound variables if, roughly, any abstraction term \(\lambda x[A]\) inside \(M\) has been replaced by \(\lambda y[A[x := y]]\).