Type soundness is now proved for expressions.

Declarations are next.