----------------------------------------------------------------------
RESQ_HALF_SPEC                                         (res_quanTools)
----------------------------------------------------------------------
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. P x ==> t}, i.e., it transforms the restricted universal
quantification to its underlying semantic representation.

      A |- !x::P. t
   --------------------  RESQ_HALF_SPEC
    A |- !x. P x ==> t


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

SEEALSO
res_quanTools.RESQ_SPEC, res_quanTools.RESQ_SPECL.

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