 Definition For \(\lambda\)-terms \(A\) and \(B\), one says that \(A\) \(\beta\)-reduces to \(B\), written \(A \rhd_{\beta} B\), if either \(A \equiv B\) or there exists a finite \(\beta\)-reduction sequence from \(A\) to \(B\).