When applied to a theorem A |- !p. t1 = t2, whose conclusion is a
paired universally quantified equation, MK_PABS returns the theorem
A |- (\p. t1) = (\p. t2).
A |- !p. t1 = t2
-------------------------- MK_PABS
A |- (\p. t1) = (\p. t2)
FAILURE
Fails unless the theorem is a (singly) paired universally quantified equation.