Specializes a theorem, with type instantiation if necessary.
DESCRIPTION
This rule specializes a quantified variable as does SPEC; it differs
from it in also instantiating the type if needed, both in the conclusion and
hypotheses:
A |- !x:ty.tm
----------------------- ISPEC `t:ty'`
A[ty'/ty] |- tm[t/x]
(where t is free for x in tm, and ty' is an instance
of ty).
FAILURE CONDITIONS
ISPEC fails if the input theorem is not universally quantified, or if
the type of the given term is not an instance of the type of the
quantified variable.
EXAMPLE
# ISPEC `0` EQ_REFL;;
val it : thm = |- 0 = 0
Note that the corresponding call to SPEC would fail because of the
type mismatch: