improve some proofs and names in ReflectiveSubuniverse.v

Because people coming from non-HoTT-land will know what `(e)transitivity` does without having to think about it, but will have to pause to think about `path_via`.