Completed the relevant proofs from Benjamin Pierce's book. The last big one in full_subtypingScript.sml is quite a complicated beast, with three inductions.
Split subtypes script up into three parts. One for basic types, and then one for each of the subtyping relations.