SWAP_EXISTS_CONV : conv
STRUCTURE
Conv
SYNOPSIS
Interchanges the order of two existentially quantified variables.
DESCRIPTION
When applied to a term argument of the form
?x y. P
, the conversion
SWAP_EXISTS_CONV
returns the theorem:
|- (?x y. P) = (?y x. P)
FAILURE
SWAP_EXISTS_CONV
fails if applied to a term that is not of the form
?x y. P
.
HOL
Kananaskis-13