RESQ_SPECL : (term list -> thm -> thm)
STRUCTURE
res_quanTools
SYNOPSIS
Specializes zero or more variables in the conclusion of a restricted universally quantified theorem.
DESCRIPTION
When applied to a term list [u1;...;un] and a theorem A |- !x1::P1. ... !xn::Pn. t, the inference rule RESQ_SPECL returns the theorem 
   A,P1 u1,...,Pn un |- t[u1/x1]...[un/xn]
where the substitutions are made sequentially left-to-right in the same way as for RESQ_SPEC, with the same sort of alpha-conversions applied to t if necessary to ensure that no variables which are free in ui become bound after substitution. 
           A |- !x1::P1. ... !xn::Pn. t
   --------------------------------------------  RESQ_SPECL "[u1;...;un]"
     A,P1 u1, ..., Pn un |- t[u1/x1]...[un/xn]
It is permissible for the term-list to be empty, in which case the application of RESQ_SPECL has no effect.
FAILURE
Fails if one of the specialization of the restricted universally quantified variable in the original theorem fails.
SEEALSO
RESQ_GEN_TAC, RESQ_SPEC
HOL  Kananaskis-10