PSELECT_ELIM expects two arguments, a theorem th1, and a pair
(p,th2): term * thm. The conclusion of th1 must have the form P($@ P),
which asserts that the epsilon term $@ P denotes some value at which
P holds. The paired variable structure p appears only in the assumption
P p of the theorem th2. The conclusion of the resulting theorem matches
that of th2, and the hypotheses include the union of all hypotheses
of the premises excepting P p.
A1 |- P($@ P) A2 u {P p} |- t
------------------------------------- PSELECT_ELIM th1 (p ,th2)
A1 u A2 |- t