Make lift and lower transparent

The reason to make them opaque was purely for typeclasses.  They will
need to be transparent when we move to trunk-polyproj, to get an
alternate version of Funext_downward_closed to work correctly.
Use NaiveFunext for proving funext_downward_closed

The new version of universe polymorphism isn't as libral with inductive
universes.  So we use NaiveFunext to allow a simpler transformation of
universes.