More progress on the declaration type soundness.

Only 2 cheated lemmas, but one isn't quite true as written :(