Make metatheory build

There are significant cheats dealing with the new application form and
new primitives in bigSmallEquiv and typeSoundness