Added a depth field to skolem variables

This will likely play a key part in implementing existential types (at least).
unifyTV signature formatting
Spec out subsumesType