improve some proofs and names in ReflectiveSubuniverse.v

Is there a reason to use `path_via` rather than `transitivity` here?