improve some proofs and names in ReflectiveSubuniverse.v

Great job cleaning up this proof!