` `

perform a generalization
Major Section: PROOF-CHECKER-COMMANDS

Example: (generalize ((and (true-listp x) (true-listp y)) 0) ((append x y) w))Generalize using the indicated substitution, which should be a non-empty list. Each element of that list should be a two-element list of the formGeneral Form: (generalize &rest substitution)

`(term variable)`

, where `term`

may use abbreviations.
The effect of the instruction is to replace each such term in the
current goal by the corresponding variable. This replacement is
carried out by a parallel substitution, outside-in in each
hypothesis and in the conclusion. More generally, actually, the
``variable'' (second) component of each pair may be `nil`

or a number,
which causes the system to generate a new name of the form `_`

or `_n`

,
with `n`

a natural number; more on this below. However, when a
variable is supplied, it must not occur in any goal of the current
proof-checker state.
When the ``variable'' above is `nil`

, the system will treat it as the
variable `|_|`

if that variable does not occur in any goal of the
current proof-checker state. Otherwise it treats it as `|_0|`

, or
`|_1|`

, or `|_2|`

, and so on, until one of these is not among the
variables of the current proof-checker state. If the ``variable''
is a non-negative integer `n`

, then the system treats it as `|_n|`

unless that variable already occurs among the current goals, in
which case it increments n just as above until it obtains a new
variable.

**Note:** The same variable may not occur as the variable component of
two different arguments (though `nil`

may occur arbitrarily many
times, as may a positive integer).