Eta conversion ($\lambda x.Mx{\equiv }_{\eta }M(x\notin FV(M))$)

Eta conversion expresses extensionality for a lambda abstraction whose fresh argument is only passed to a function. The side condition prevents removal of a genuine dependency. In a categorical model with $D\cong D^D$, the inverse laws for currying and evaluation validate this conversion as well as beta reduction.