Get the metatheory building again

There is one cheat in type soundness because equality types are not
implemented yet, but now = fails when one of its arguments contains a
closure.