Suggestion on Document: Explicit Declaration for Multiple Universe Level Variable

Hello Lean Developer,

I was writing universe-lifting function due to lack of cumulative universe

inductive  liftU.{u v}  (X: Type u) : Type (max v (u + 1)) := 
  | inh : X → liftU X

It doesn't work, and I was stuck on the document for a while, not sure if explicit universe-level variable declaration can be done.

Then my friend told me I have to add a comma between u and v for multiple variables. Problem solved.

I think document it would be of great help.

When I was trying all sorts of syntax, I bump into the following seemingly working.

inductive LiftU {u : Type x} {v : Type y} (X : Type u) : Type (max v (u + 1)) :=
  | inh : X → LiftU X

I wonder if this is an intended behaviour (i.e. universe level type is some Type _). Also wonder if the above level x y for the level u v would impact anything.

I believe documenting these would be of great help for the Lean beginner, great thanks!