----------------------------------------------------------------------
PSELECT_CONV                                               (PairRules)
----------------------------------------------------------------------
PSELECT_CONV : conv

KEYWORDS
conversion, epsilon.

LIBRARY
pair

SYNOPSIS
Eliminates a paired epsilon term by introducing an existential quantifier.

DESCRIBE
The conversion {PSELECT_CONV} expects a boolean term of the form
{"t[@p.t[p]/p]"}, which asserts that the epsilon term {@p.t[p]} denotes
a pair, {p} say, for which {t[p]} holds.  This assertion is equivalent
to saying that there exists such a pair, and {PSELECT_CONV} applied to a
term of this form returns the theorem {|- t[@p.t[p]/p] = ?p. t[p]}.

FAILURE
Fails if applied to a term that is not of the form {"p[@p.t[p]/p]"}.

SEEALSO
Conv.SELECT_CONV, PairRules.PSELECT_ELIM, PairRules.PSELECT_INTRO,
PairRules.PSELECT_RULE.

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