PAIRED_ETA_CONV : conv
STRUCTURE
PairedLambda
SYNOPSIS
Performs generalized eta conversion for tupled eta-redexes.
DESCRIPTION
The conversion PAIRED_ETA_CONV generalizes ETA_CONV to eta-redexes with tupled abstractions. 
   PAIRED_ETA_CONV   \(v1..(..)..vn). f (v1..(..)..vn)
    = |- \(v1..(..)..vn). f (v1..(..)..vn) = f

FAILURE
Fails unless the given term is a paired eta-redex as illustrated above.
COMMENTS
Note that this result cannot be achieved by ordinary eta-reduction because the tupled abstraction is a surface syntax for a term which does not correspond to a normal pattern for eta reduction. Taking the term apart reveals the true form of a paired eta redex: 
   - dest_comb (Term `\(x:num,y:num). FST (x,y)`)
   > val it = (`UNCURRY`, `\x y. FST (x,y)`) : term * term

EXAMPLE
The following is a typical use of the conversion: 
   val SELECT_PAIR_EQ = Q.prove
    (`(@(x:'a,y:'b). (a,b) = (x,y)) = (a,b)`,
     CONV_TAC (ONCE_DEPTH_CONV PairedLambda.PAIRED_ETA_CONV) THEN
     ACCEPT_TAC (SYM (MATCH_MP SELECT_AX (REFL (Term `(a:'a,b:'b)`)))));
SEEALSO
ETA_CONV
HOL  Kananaskis-13