improve some proofs and names in ReflectiveSubuniverse.v

Note that you don't need to include `(fun f => f o (O_unit subU P))`, and can just use an underscore; it'll be inferred from the `IsEquiv` argument.  (If your inclusion of it was intentional, ignore this comment.)