When applied to a term list [x1,...,xn] and a theorem A |- t, the inference
rule GENL returns the theorem A |- !x1...xn. t, provided none of the
variables xi are free in any of the assumptions. It is not necessary that
any or all of the xi should be free in t.
A |- t
------------------ GENL [x1,...,xn] [where no xi is free in A]
A |- !x1...xn. t