SPECL : term list -> thm -> thm
A |- !x1...xn. t -------------------------- SPECL [`u1`;...;`un`] A |- t[u1/x1]...[un/xn]
# let t = ARITH_RULE `!m n p q. m <= p /\ n <= q ==> (m + n) <= (p + q)`;; val t : thm = |- !m n p q. m <= p /\ n <= q ==> m + n <= p + q # SPECL [`1`; `2`; `3`; `4`] t;; val it : thm = |- 1 <= 3 /\ 2 <= 4 ==> 1 + 2 <= 3 + 4