Move some things out of Misc, add hProp lemmas

We now have better support for paths of hProps