ETA_CONV : conv
STRUCTURE
SYNOPSIS
Performs a toplevel eta-conversion.
DESCRIPTION
ETA_CONV maps an eta-redex \x. (t x), where x does not occur free in t, to the theorem |- (\x. (t x)) = t.
FAILURE
Fails if the input term is not an eta-redex.
SEEALSO
HOL  Kananaskis-13