improve some proofs and names in ReflectiveSubuniverse.v

Do we have a convention on when we lowercase capital names, and when we don't?  e.g., [`path_unit`](https://github.com/HoTT/HoTT/blob/master/theories/types/Unit.v#L31) for `Unit`.