simplify proof of sigma_subuniverse and rename