The command

The command `resume by generalizing x from t` directs LP to resume the proof
of the current conjecture by this method.

This proof method, which eliminates a universal quantifier from a conjecture,
is the dual of the fix command, which eliminates an existential
quantifier from a fact. It is subject to restrictions on `x` and `t` as
for the fix command.

This command is unlikely to be used when `F` contains free variables other
than `x`. When `x` is the only free variable in `F`, the only
restriction is that `t` be a constant that does not occur in `F` or in
any fact in LP's logical system. For example, the command

is allowed whenprove \A x (f(x) = c) by generalizing x from d