` `

move antecedents of conclusion's `implies`

term to top-level
` `

hypotheses
Major Section: PROOF-CHECKER-COMMANDS

Examples: promote (promote t)For example, if the conclusion is

`(implies (and x y) z)`

, then
after execution of `promote`

, the conclusion will be `z`

and the terms `x`

and `y`

will be new top-level hypotheses.

General Form: (promote &optional do-not-flatten-flag)Replace conclusion of

`(implies hyps exp)`

or `(if hyps exp t)`

with
simply `exp`

, adding `hyps`

to the list of top-level hypotheses.
Moreover, if `hyps`

is viewed as a conjunction then each conjunct will
be added as a separate top-level hypothesis. An exception is that
if `do-not-flatten-flag`

is supplied and not `nil`

, then only one
top-level hypothesis will be added, namely `hyps`

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

.