Generalizes the conclusion of a theorem over its own free variables.
DESCRIPTION
When applied to a theorem A |- t, the inference rule GEN_ALL
returns the theorem A |- !x1...xn. t, where the xi are all the
variables, if any, which are free in t but not in the assumptions.
A |- t
------------------ GEN_ALL
A |- !x1...xn. t
FAILURE
Never fails.
COMMENTS
Sometimes people write code that depends on the order of the
quantification. They shouldn’t.