 Definition (one-step \(\eta\)-reduction) For \(\lambda\)-terms \(A\) and \(B\), we say that \(A\) \(\beta \eta\)-reduces in one step to \(B\), written \(A \rhd_{\beta \eta ,1} B\), just in case there exists an (occurrence of a) subterm \(C\) of \(A\), a variable \(x\), and \(\lambda\)-terms \(M\) and \(N\) such that either