## 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.