cleaned up a bunch of proofs about target types
re-proved regularity of typing judgment; stated desired properties for contexts