Subgoal *1/2 is the induction step from the scheme, obtained by
instantiating the scheme with our conjecture.
We number the cases ``backward'', so this is case ``2'' of the
proof of ``*1''. We number them backward so you can look at a subgoal
number and get an estimate for how close you are to the end.