Reduces paired existentially quantified goal to one involving a
specific witness.
DESCRIPTION
When applied to a term q and a goal ?p. t, the tactic
PEXISTS_TAC reduces the goal to t[q/p].
A ?- ?p. t
============= EXISTS_TAC "q"
A ?- t[q/p]
FAILURE
Fails unless the goal’s conclusion is a paired existential quantification
and the term supplied has the same type as the quantified pair in the goal.