improve some proofs and names in ReflectiveSubuniverse.v

`[O(A*B) = OA * OB]`?