improve some proofs and names in ReflectiveSubuniverse.v

`[O(A*B)]`?