 Definition (one-step \(\beta \eta\)-reduction) \(\lambda x[Mx] \rhd_{\beta \eta ,1} M\) and \((\lambda x[M]N)) \rhd_{\beta \eta ,1} M[x := N]\). A \(\lambda\)-term \(A\) \(\beta \eta\)-reduces in one step to a \(\lambda\)-term \(B\) just in case either \(A\) \(\beta\)-reduces to \(B\) in one step or \(A\) \(\eta\)-reduces to \(B\) in one step.