INST_TYPE : (hol_type * hol_type) list -> thm -> thm
A |- t ----------------------------------- INST_TYPE [ty1,tv1;...;tyn,tvn] A[ty1,...,tyn/tv1,...,tvn] |- t[ty1,...,tyn/tv1,...,tvn]
# SPECL [`a:num`; `b:num`] EQ_SYM_EQ ;; Exception: Failure "SPECL".
# SPECL [`a:num`; `b:num`] (INST_TYPE [`:num`,`:A`] EQ_SYM_EQ) ;; val it : thm = |- a = b <=> b = a