Fix [change] forgeting about universes in the right-hand-side (#36) and better fix for #35 and #37,
disallowing only Set/Set+1 <= Prop constraints.
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).