improve some proofs and names in ReflectiveSubuniverse.v