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.
The returned theorem asserts that $@ P denotes some value
at which P holds.
A |- P x
A |- P($@ P)