RIGHT_ETA : thm -> thm
STRUCTURE
Drule
SYNOPSIS
Perform one step of eta-reduction on the right hand side of an equational theorem.
DESCRIPTION
    A |- M = (\x. (N x))
   ---------------------   x not free in N
    A |- M = N

FAILURE
If the right hand side of the equation is not an eta-redex, or if the theorem is not an equation.
EXAMPLE
- val INC_DEF = new_definition ("INC_DEF", Term`INC = \x. 1 + x`);
> val INC_DEF = |- INC = (\x. 1 + x) : thm

- RIGHT_ETA INC_DEF;
> val it = |- INC = $+ 1 : thm

SEEALSO
ETA_CONV, eta_conv
HOL  Kananaskis-10