improve some proofs and names in ReflectiveSubuniverse.v

Well, is there a reason to use `(e)transitivity` rather than `path_via`?  (-: