Added supporting text to both the type system and the proofs.  Still
need to give a basic outline of types in the type system section.