UNCURRY_EXISTS_CONV : conv
STRUCTURE
PairRules
LIBRARY
pair
SYNOPSIS
Uncurrys consecutive existential quantifications into a paired existential quantification.
EXAMPLE
- UNCURRY_EXISTS_CONV (Term `?x y. x + y = y + x`);
> val it = |- (?x y. x + y = y + x) = ?(x,y). x + y = y + x : thm

- UNCURRY_EXISTS_CONV (Term `?(w,x) (y,z). w+x+y+z = z+y+x+w`);
> val it =
    |- (?(w,x) (y,z). w + x + y + z = z + y + x + w) =
       ?((w,x),y,z). w + x + y + z = z + y + x + w : thm

FAILURE
UNCURRY_EXISTS_CONV tm fails if tm is not a consecutive existential quantification.
SEEALSO
CURRY_CONV, UNCURRY_CONV, CURRY_EXISTS_CONV, CURRY_FORALL_CONV, UNCURRY_FORALL_CONV
HOL  Kananaskis-14