 Definition (substitution) We write ‘\(M[x := N]\)’ to denote the substitution of \(N\) for the free occurrences of \(x\) in \(M\). A precise  definition[2]  by recursion on the set of \(\lambda\)-terms is as follows: for all terms \(A\), \(B\), and \(M\), and for all variables \(x\) and \(y\), we define