 The first clause in the definition of \(\rhd_{\beta \eta ,1}\) ensures that the relation extends the relation of one-step \(\beta\)-reduction. As we did for the relation of one-step \(\beta\)-reduction, we can replay the development for \(\eta\)-reduction. Thus, one has the notion of an \(\eta\)-redex, and from \(\rhd_{\eta ,1}\) one can define the relation \(\rhd_{\eta}\) between \(\lambda\)-terms as the symmetric and transitive closure of \(\rhd_{\eta ,1}\), which captures zero-or-more-steps of \(\eta\)-reduction. Then one defines \(=_{\eta}\) as the symmetric and transitive closure of \(\rhd_{\eta}\).