The conversion PEXISTS_CONV expects a boolean term of the form
(?p. t[p]), where p may be a paired structure or variables,
and converts it to the form (t [@p. t[p]]).
--------------------------------- PEXISTS_CONV "(?p. t[p])"
(|- (?p. t[p]) = (t [@p. t[p]])