Type soundness proved (finally)
Delete cruft
The metatheory directory builds again