Moving theorems to HOL

So this now requires an up-to-date HOL to build
More fixes for theorems moving to HOL.

NB, I haven't tested everything yet.