apply one instruction to current goal and another to new subgoals
Major Section: PROOF-CHECKER-COMMANDS
Example: (then induct prove) General Form: (then first-instruction &optional completion must-succeed-flg)Run
first-instruction, and then run completion (another
instruction) on each subgoal created by first-instruction. If
must-succeed-flg is supplied and not nil, then halt at the first
``failure'' and remove the effects of the invocation of completion that
``failed''.The default for completion is reduce.
