Following new development up to subtyping transitivity.

TODO:
- For the environment, we still do a lookup globally, so for overwritten
vars that might be a problem. Do the stratified wf-env instead.
- Finish type safety proof following Tiark's test7.elf.