Minor cleanup of Lemma 4

- Removes some equation numbers that were unused
- Makes a few minor changes to the wording.
Merge branch 'lemma_4'

This branch makes a few minor changes to Lemma 4 and was the result
of an audit of its proof. The proof should be viewed as correct and
verified now.

Closes #8