The inference rule PSELECT_RULE expects a theorem asserting the
existence of a pair p such that t holds. The equivalent assertion
that the epsilon term @p.t denotes a pair p for
which t holds is returned as a theorem.
A |- ?p. t
------------------ PSELECT_RULE
A |- t[(@p.t)/p]