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