improve some proofs and names in ReflectiveSubuniverse.v

By which I might mean `etransitivity`.  However, we might have a sufficiently new version of trunk that we can redefine `transitivity` and `symmetry`.