LP, the Larch Prover — Proofs by specialization

The command prove F by specializing x to t directs LP to prove a formula F by creating a single subgoal in which all accessible prenex-existential quantifiers over the variable x have been eliminated from F and all occurrences of x bound by those quantifier have been replaced by t.

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

prove \A x \E y (x < y) by specializing y to s(x)

reduces the proof of the conjecture to establishing the subgoal x < s(x).