Specializes the conclusion of a theorem, returning the chosen variant.
DESCRIPTION
When applied to a theorem A |- !p. t, the inference rule PSPEC_PAIR
returns the term q' and the theorem A |- t[q'/p], where q' is a variant
of p chosen to avoid free variable capture.
A |- !p. t
-------------- PSPEC_PAIR
A |- t[q'/q]
FAILURE
Fails unless the theorem’s conclusion is a paired universal quantification.
COMMENTS
This rule is very similar to plain PSPEC, except that it returns the
variant chosen, which may be useful information under some circumstances.