+{- Note [Type substitution]
+ ~~~~~~~~~~~~~~~~~~~~~~~~
+Why do we need a type substitution? Consider
+ /\(a:*). \(x:a). /\(a:*). id a x
+This is ill typed, because (renaming variables) it is really
+ /\(a:*). \(x:a). /\(b:*). id b x
+Hence, when checking an application, we can't naively compare x's type
+(at its binding site) with its expected type (at a use site). So we
+rename type binders as we go, maintaining a substitution.
+
+The same substitution also supports let-type, current expressed as
+ (/\(a:*). body) ty
+Here we substitute 'ty' for 'a' in 'body', on the fly.
+-}
+