PEXISTS_CONV : conv
STRUCTURE
LIBRARY
pair
SYNOPSIS
Eliminates paired existential quantifier by introducing a paired choice-term.
DESCRIPTION
The conversion PEXISTS_CONV expects a boolean term of the form (?p. t[p]), where p may be a paired structure or variables, and converts it to the form (t [@p. t[p]]).
   ---------------------------------  PEXISTS_CONV "(?p. t[p])"
    (|- (?p. t[p]) = (t [@p. t[p]])

FAILURE
Fails if applied to a term that is not a paired existential quantification.
SEEALSO
HOL  Kananaskis-13