ACL2-PC::CG

(macro) change to another goal.
Major Section:  PROOF-CHECKER-COMMANDS

Examples:
(cg (main . 1)) -- change to the goal (main . 1)
cg              -- change to the next-to-top goal

General Form:
(CG &OPTIONAL goal-name)
Same as (change-goal goal-name t), i.e. change to the indicated and move the current goal to the end of the goal stack.