globla environment和local context

看了coq art，解决了一个长期以来的猜想，即globla environment和local context实际上是同种sort。
这意味着，在非meta-language的意义上，两者具有相同的sort，都是由definition和declaration组成的list。