 The understanding is that we can reduce or contract \((\rhd)\) an application \((\lambda xM)N\) of an abstraction term (the left-hand side, \(\lambda xM)\) to something (the right-hand side, \(N)\) by simply plugging in \(N\) for the occurrences of \(x\) inside \(M\) (that’s what the notation ‘\(M[x := N]\)’ expresses).  \(\beta\)-reduction, or \(\beta\)-conversion, is the heart of the \(\lambda\)-calculus.  When one actually applies \(\beta\)-reduction to reduce a term, there is an important proviso that has to be observed. But this will be described in Section 2.1, when we discuss bound and free variables.