----------------------------------------------------------------------
SWAP_PFORALL_CONV                                          (PairRules)
----------------------------------------------------------------------
SWAP_PFORALL_CONV : conv

KEYWORDS
conversion, quantifier, existential.

LIBRARY
pair

SYNOPSIS
Interchanges the order of two universally quantified pairs.

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

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




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

SEEALSO
PairRules.SWAP_PEXISTS_CONV.

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