improve some proofs and names in ReflectiveSubuniverse.v

Should `(O T)` be in square brackets for coqdoc?  (And `((O P)->Q) <~> (P -> Q)` below, too?)