Abduction: another way to detect bad applications of induction

[yutakang]

1. We apply the induct tactic.
2. We get a step case whose shape looks like induction_hypothesis ==> conclusion.
3. Take conclusion from this step case.
4. Apply clarsimp to theconclusion`.
5. If there is a remaining goal, then call it conclusion1, else decide that the induction was not bad.
6. Apply clarsimp to the entire step case induction_hypothesis ==> conclusion.
7. If there is a remaining goal of the form of induction_hypothesis2 ==> conclusion2, then take conclusion2, else decide that the induction was not bad.
8. Compare conclusion1 against conclusion2.
9. If they are different, then decide that the induction was not bad, else the induction was not useful.

If at least one subgoal is "was not bad", then the induction was "useful".

[yutakang]

I need a concrete example for this.