SWAP_PFORALL_CONV : conv
STRUCTURE
LIBRARY
pair
SYNOPSIS
Interchanges the order of two universally quantified pairs.
DESCRIPTION
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
HOL  Kananaskis-10