Make type levels more canonical

* src/lexp.ml (sort_level): Replace SLn with SLz.
(lexp_location, _lexp_to_str): Adjust accordingly.

* src/opslexp.ml (sort_level_max): New function.
(sort_compose): Use it.
(impredicative_erase): New var.
(check): Adjust for new SLz.  Obey impredicative_erase.
Fix level calculation for inductive types.

* src/builtin.ml (type0, type1, type2): Adjust.