Start fixing up the proof of 3.6 after tweaking the statement.

Fill in TODOs and easy cases.