More progress on the metatheory directory

It all builds mow, but there are some missing results in
bigBigEquivScript.