----------------------------------------------------------------------
PSELECT_INTRO                                              (PairRules)
----------------------------------------------------------------------
PSELECT_INTRO : (thm -> thm)

KEYWORDS
rule, epsilon.

LIBRARY
pair

SYNOPSIS
Introduces an epsilon term.

DESCRIBE
{PSELECT_INTRO} takes a theorem with an applicative conclusion, say
{P x}, and returns a theorem with the epsilon term {$@ P} in place
of the original operand {x}.

     A |- P x
   --------------  PSELECT_INTRO
    A |- P($@ P)

The returned theorem asserts that {$@ P} denotes some value
at which {P} holds.

FAILURE
Fails if the conclusion of the theorem is not an application.

COMMENTS
This function is exactly the same as {SELECT_INTRO}, it is duplicated in
the pair library for completeness.

SEEALSO
Drule.SELECT_INTRO, PairRules.PEXISTS, PairRules.PSELECT_CONV,
PairRules.PSELECT_ELIM, PairRules.PSELECT_RULE.

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