SPECL : term list -> thm -> thm
STRUCTURE
SYNOPSIS
Specializes zero or more variables in the conclusion of a theorem.
DESCRIPTION
When applied to a term list [u1;...;un] and a theorem A |- !x1...xn. t, the inference rule SPECL returns the theorem A |- t[u1/x1]...[un/xn], where the substitutions are made sequentially left-to-right in the same way as for 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...xn. t
   --------------------------  SPECL [u1,...,un]
     A |- t[u1/x1]...[un/xn]
It is permissible for the term-list to be empty, in which case the application of SPECL has no effect.
FAILURE
Fails unless each of the terms is of the same type as that of the appropriate quantified variable in the original theorem.
EXAMPLE
The following is a specialization of a theorem from theory arithmetic.
   - arithmeticTheory.LESS_EQ_LESS_EQ_MONO;
   > val it = |- !m n p q. m <= p /\ n <= q ==> m + n <= p + q : thm

   - SPECL (map Term [`1`, `2`, `3`, `4`]) it;
   > val it = |- 1 <= 3 /\ 2 <= 4 ==> 1 + 2 <= 3 + 4 : thm

SEEALSO
HOL  Kananaskis-13