PSELECT_INTRO
PairRules.PSELECT_INTRO : (thm -> thm)
Introduces an epsilon term.
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.
See also
Drule.SELECT_INTRO,
PairRules.PEXISTS,
PairRules.PSELECT_CONV,
PairRules.PSELECT_ELIM,
PairRules.PSELECT_RULE