`PALPHA_CONV : term -> conv`
STRUCTURE
LIBRARY
pair
SYNOPSIS
Renames the bound variables of a paired lambda-abstraction.
DESCRIPTION
If q is a variable of type ty and \p.t is a paired abstraction in which the bound pair p also has type ty, then ALPHA_CONV q "\p.t" returns the theorem:
```   |- (\p.t) = (\q'. t[q'/p])
```
where the pair q':ty is a primed variant of q chosen so that none of its components are free in \p.t. The pairs p and q need not have the same structure, but they must be of the same type.
EXAMPLE
PALPHA_CONV renames the variables in a bound pair:
```   - PALPHA_CONV
(Term `((w:'a,x:'a),(y:'a,z:'a))`)
(Term `\((a:'a,b:'a),(c:'a,d:'a)). (f a b c d):'a`);
> val it = |- (\((a,b),c,d). f a b c d) = (\((w,x),y,z). f w x y z) : thm
```

The new bound pair and the old bound pair need not have the same structure.

```   - PALPHA_CONV
(Term `((wx:'a#'a),(y:'a,z:'a))`)
(Term `\((a:'a,b:'a),(c:'a,d:'a)). (f a b c d):'a`);
> val it = |- (\((a,b),c,d). f a b c d) =
(\(wx,y,z). f (FST wx) (SND wx) y z) : thm
```
PALPHA_CONV recognises subpairs of a pair as variables and preserves structure accordingly.
```   - PALPHA_CONV
(Term `((wx:'a#'a),(y:'a,z:'a))`)
(Term `\((a:'a,b:'a),(c:'a,d:'a)). (f (a,b) c d):'a`);
> val it = |- (\((a,b),c,d). f (a,b) c d) = (\(wx,y,z). f wx y z) : thm
```