improve lift and lower

What's the reason to give the universes explicitly here?  (Will Coq collapse them if you don't?)  (I think you should either not give the universes explicitly, both in `lift'` and `lower'` and `isequiv_lift'`, or you should add a comment about why you're doing it.)