When applied to a theorem A |- !x::P. t, the derived inference rule
RESQ_HALF_SPEC returns the theorem A |- !x. x IN P ==> t, i.e., it
transforms the restricted universal quantification to its underlying
semantic representation.
A |- !x::P. t
-------------------- RESQ_HALF_SPEC
A |- !x. x IN P ==> t