ACL2-PC::WRAP-INDUCT

(atomic macro) same as induct, but create a single goal
Major Section:  PROOF-CHECKER-COMMANDS

Examples:
wrap-induct
(wrap-induct t)
(wrap-induct (append (reverse x) y))

General Form: (wrap-induct &optional term)

The wrap-induct command is identical to the proof-checker induct command, except that only a single goal is created: the conjunction of the base and induction steps.

Note: The output will generally indicate that more than goal has been created, e.g.:

Creating two new goals:  (MAIN . 1) and (MAIN . 2).
However, wrap-induct always creates a unique goal (when it succeeds). A subsequent message clarifies this, for example:
NOTE: Created ONLY one new goal, which is the current goal:
  (MAIN . 1)