 As before with the reflexivity rule, the rule \(\boldsymbol{\beta}\) has no premises: for any variable \(x\) and any terms \(M\) and \(A\), one can infer the equation \((\lambda x[M])A = M[x := A]\) at any point in a formal derivation in the theory \(\boldsymbol{\lambda}\).