----------------------------------------------------------------------
PSELECT_RULE                                               (PairRules)
----------------------------------------------------------------------
PSELECT_RULE : (thm -> thm)

KEYWORDS
rule, epsilon.

LIBRARY
pair

SYNOPSIS
Introduces a paired epsilon term in place of a paired existential quantifier.

DESCRIBE
The inference rule {PSELECT_RULE} expects a theorem asserting the
existence of a pair {p} such that {t} holds.  The equivalent assertion
that the epsilon term {@p.t} denotes a pair {p} for
which {t} holds is returned as a theorem.

       A |- ?p. t
   ------------------  PSELECT_RULE
    A |- t[(@p.t)/p]




FAILURE
Fails if applied to a theorem the conclusion of which is not
a paired existential quantifier.

SEEALSO
Drule.SELECT_RULE, PairRules.PCHOOSE, PairRules.PSELECT_CONV,
PairRules.PEXISTS_CONV, PairRules.PSELECT_ELIM,
PairRules.PSELECT_INTRO.

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