eliminate funext (mostly) in ReflectiveSubuniverse.v