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].