Specializes the conclusion of a universal theorem.
DESCRIPTION
When applied to a term u and a theorem A |- !x. t,
Specialize returns the theorem A |- t[u/x]. Care is taken
to ensure that no variables free in u become bound after
this operation.
A |- !x. t
-------------- Specialize u
A |- t[u/x]
FAILURE
Fails if the theorem’s conclusion is not universally quantified,
or if x and u have different types.
COMMENTS
Specialize behaves identically to SPEC, but is faster.