----------------------------------------------------------------------
SWAP_PEXISTS_CONV                                          (PairRules)
----------------------------------------------------------------------
SWAP_PEXISTS_CONV : conv

KEYWORDS
conversion, quantifier, existential.

LIBRARY
pair

SYNOPSIS
Interchanges the order of two existentially quantified pairs.

DESCRIBE
When applied to a term argument of the form {?p q. t}, the conversion
{SWAP_PEXISTS_CONV} returns the theorem:

   |- (?p q. t) = (?q t. t)




FAILURE
{SWAP_PEXISTS_CONV} fails if applied to a term that is not of the form
{?p q. t}.

SEEALSO
Conv.SWAP_EXISTS_CONV, PairRules.SWAP_PFORALL_CONV.

----------------------------------------------------------------------