RESQ_SPEC : term -> thm -> thm
STRUCTURE
res_quanLib
SYNOPSIS
Specializes the conclusion of a possibly-restricted universally quantified theorem.
DESCRIPTION
When applied to a term u and a theorem A |- !x::P. t, RESQ_SPEC returns the theorem A, u IN P |- t[u/x]. If necessary, variables will be renamed prior to the specialization to ensure that u is free for x in t, that is, no variables free in u become bound after substitution. 
      A |- !x::P. t
   ---------------------  RESQ_SPEC "u"
    A, u IN P |- t[u/x]
Additionally, if the input theorem is a standard universal quantification, then RESQ_SPEC behaves like SPEC.
FAILURE
Fails if the theorem’s conclusion is not restricted universally quantified, or if type instantiation fails.
SEEALSO
RESQ_HALF_SPECL
HOL  Trindemossen-1