move to the parent (or some ancestor) of the current subterm
Major Section: PROOF-CHECKER-COMMANDS
Examples: if the conclusion is (= x (* (- y) z)) and the
current subterm is y, then we have:
up or (up 1) -- the current subterm becomes (- y)
(up 2) -- the current subterm becomes (* (- y) z)
(up 3) -- the current subterm becomes the entire conclusion
(up 4) -- no change; can't go up that many levels
General Form:
(up &optional n)
Move up n levels in the conclusion from the current subterm, where n
is a positive integer. If n is not supplied or is nil, then move up
1 level, i.e., treat the instruction as (up 1).See also dive, top, nx, and bk.
