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-14