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.