GENL : term list -> thm -> thm
A |- t ------------------ GENL `[x1;...;xn]` [where no xi is free in A] A |- !x1...xn. t
# SPEC `m + p:num` ADD_SYM;; val it : thm = |- !n. (m + p) + n = n + m + p # GENL [`m:num`; `p:num`] it;; val it : thm = |- !m p n. (m + p) + n = n + m + p