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.