All universe levels must be strictly positive. Unless otherwise stated the tokens `nil` and `NIL` may be used as identifiers to indicate that no identifier should label the new hypothesis.
