Eta conversion
= Eta conversion
{title2=$\lambda x.Mx\equiv_\eta M\quad(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>.