WLS: updated the discussion of subtyping to include proper definitions of subtype soundness and completeness.  The formalisation of types is now looking rather nice.