As for your follow-up question: Coq implements η-conversion, but not η-reduction/expansion, because η really is treated at the level of the conversion test and not at that of reduction (which is a sub-routine thereof). Concretely, the conversion test works roughly as follows when comparing
u to weak head normal forms (using a bunch of reduction rules including β but not η)
- if one of the reducts is a neutral
n and the other is an abstraction
fun x : A => t, recursively compare
n x and
t (this corresponds to η-expanding the neutral followed by a congruence rule for abstraction)
The reasons to do things like this are a bit tricky, but the bottom line is that implementing η inside reduction (be it as expansion or reduction) would either break good properties or simply be unfeasable in current Coq.
I did a talk about this at WITS a few weeks ago, the video does not seem to be up on Youtube yet (it should be there at some point) but the slides and abstract are on my page.