apply one instruction to current goal and another to new subgoals
(then induct prove)
(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
The default for completion is reduce.