Fix weaken_sort_scheme and disallow equating global universes with Prop
or Set, they should be initially declared as such sorts instead (never
happens in the standard library).