Started work on type soundness with signatures.

This required removing the type annotations on variable uses (for their
type applications) to get the necessary weakening property to hold:

signature S = sig
 val f : int -> int
end

structure S :> S = struct
 val f x = x
end

val _ = f 4

Given
(f : int -> int) |- f : int -> int

you have to prove that

(f : forall 'a. 'a -> 'a) |- f : int -> int

the substitution changes from [] to [('a, int)], so we don't want it
annotated in the term.

This is work in progress.