SWAP_PEXISTS_CONV
PairRules.SWAP_PEXISTS_CONV : conv
Interchanges the order of two existentially quantified pairs.
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.