SWAP_PFORALL_CONV : conv
STRUCTURE
PairRules
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
SWAP_PEXISTS_CONV
HOL
Kananaskis-14