(* Max of non-empty list of named universes, or their successor (when true)
* The empty list represents type0 *)
type sort = Prop | Type of universe
type implicit_annotation =
(* Max of non-empty list of named universes, or their successor (when true)
* The empty list represents type0 *)
type sort = Prop | Type of universe
type implicit_annotation =