This is still a rather horrible proof, though. More work to be done.