Fix clear of section variables that are no longer allowed.
Avoid unnecessary abstraction over level variables when rewriting with paths.
Cleanup the proof that Unit is an hSet.
Thanks to less spurious quantifications on levels, the universe instance is shortened here.