 \(\eta\)-Contraction. Replace a well-formed part \([\lambda \by_{\beta}[\bB_{\alpha \beta}\by_{\beta}]]\) of a wff by \(\bB_{\alpha \beta}\), provided \(\by_{\beta}\) does not occur free in \(\bB_{\alpha \beta}\).