improve some proofs and names in ReflectiveSubuniverse.v

I don't remember whether it was intentional when I wrote it, but right now my inclination is to leave it as documentation.