----------------------------------------------------------------------
SWAP_EXISTS_CONV                                                (Conv)
----------------------------------------------------------------------
SWAP_EXISTS_CONV : conv

SYNOPSIS
Interchanges the order of two existentially quantified variables.

KEYWORDS
conversion, quantifier, existential.

DESCRIBE
When applied to a term argument of the form {?x y. P}, the conversion
{SWAP_EXISTS_CONV} returns the theorem:

   |- (?x y. P) = (?y x. P)




FAILURE
{SWAP_EXISTS_CONV} fails if applied to a term that is not of the form
{?x y. P}.

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