` `

move top-level hypotheses to the conclusion
Major Section: PROOF-CHECKER-COMMANDS

Examples: demote -- demote all top-level hypotheses (demote 3 5) -- demote hypotheses 3 and 5For example, if the top-level hypotheses are

`x`

and `y`

and the
conclusion is `z`

, then after execution of `demote`

, the conclusion will
be `(implies (and x y) z)`

and there will be no (top-level)
hypotheses.

General Form: (demote &rest hyps-indices)Eliminate the indicated (top-level) hypotheses, but replace the conclusion

`conc`

with `(implies hyps conc)`

where `hyps`

is the
conjunction of the hypotheses that were eliminated. If no arguments
are supplied, then all hypotheses are demoted, i.e. `demote`

is the
same as `(demote 1 2 ... n)`

where `n`

is the number of top-level
hypotheses.
**Note**: You must be at the top of the conclusion in order to use
this command. Otherwise, first invoke `top`

. Also, `demote`

fails if
there are no top-level hypotheses or if indices are supplied that
are out of range.