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