improve some proofs and names in ReflectiveSubuniverse.v

If we can reduce the number of tactics by going to standard ones that would be great.
Has Coq improved enough for this? I also note that many instances of refine can be replaced by apply now.