ACL2-PC::DEMOTE

(primitive) 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 5
For 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.