PSELECT_CONV
PairRules.PSELECT_CONV : conv
Eliminates a paired epsilon term by introducing an existential quantifier.
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]".
See also
Conv.SELECT_CONV,
PairRules.PSELECT_ELIM,
PairRules.PSELECT_INTRO,
PairRules.PSELECT_RULE