----------------------------------------------------------------------
PEXISTS_CONV                                               (PairRules)
----------------------------------------------------------------------
PEXISTS_CONV : conv

KEYWORDS
conversion, epsilon.

LIBRARY
pair

SYNOPSIS
Eliminates paired existential quantifier by introducing a paired choice-term.

DESCRIBE
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
PairRules.PSELECT_RULE, PairRules.PSELECT_CONV,
PairRules.PEXISTS_RULE, PairRules.PSELECT_INTRO,
PairRules.PSELECT_ELIM.

----------------------------------------------------------------------