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)