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 when d is a new constant and reduces the proof of the conjecture to establishing the subgoal f(d) = c. See Skolem-constant.prove \A x (f(x) = c) by generalizing x from d