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 existential quantifiers from a conjecture, is the dual of the instantiate command, which eliminates universal quantifiers from facts.

For example, the command

reduces the proof of the conjecture to establishing the subgoalprove \A x \E y (x < y) by specializing y to s(x)