Eta equivalence

A relation that relates a term to its Eta-expansion - $\lambda x.\ f\ x =_\eta f$ when $x \notin FV(f)$ - capturing the principle that functions with identical input-output behavior are equivalent.