----------------------------------------------------------------------
RESQ_HALF_SPEC                                           (res_quanLib)
----------------------------------------------------------------------
RESQ_HALF_SPEC : thm -> thm

SYNOPSIS
Strip a restricted universal quantification in the conclusion of a theorem.

KEYWORDS
rule, restricted quantifier.

DESCRIBE
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


FAILURE
Fails if the theorem’s conclusion is not a restricted universal quantification.

SEEALSO
res_quanLib.RESQ_SPEC.

----------------------------------------------------------------------