SWAP_PEXISTS_CONV : conv

- STRUCTURE
- LIBRARY
- pair
- SYNOPSIS
- Interchanges the order of two existentially quantified pairs.
- DESCRIPTION
- 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

HOL Kananaskis-14