On the Naming of Subgoals
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.