Small layout changes.
Finish up to lemma 5/29.10