Use NaiveFunext for proving funext_downward_closed

The new version of @mattam82's universe polymorphism isn't as libral
with inductive universes.  So we use NaiveFunext to allow a simpler
transformation of universes.

This is in preparation for switching to Coq trunk, once enough bugs are fixed.