Work toward the new type system check for completeness.

There's now a cheat in the soundness proof, since there's an extra
condition that the type system requires.