 As with the square brackets employed to write abstraction terms, the square brackets employed to write substitution are not officially part of the syntax of the \(\lambda\)-calculus. \(M\) and A are terms, \(x\) is a variable; \(M[x := A]\) is another term.