refactor(*): remove universes command

[Julian]

This makes universe take multiple universe parameters,
making it consistent with variable (which has subsumed
Lean 3's variables.

Hopefully I've done this correctly, I had to do a bit of a dance when running make update-stage0 because otherwise even Init/Prelude.lean couldn't be built, but obviously let me know if this is totally off.

This touches lots of files obviously (sorry), but I think if I've done it correctly, the only real changes are to src/Lean/Parser/Command.lean and src/Lean/Elab/Command.lean.

[leodemoura]

Thanks for trying to help, but this kind of PR is more distracting than useful.
This is not how we apply this kind of change. The update stage0 steps require coordination. Right now, only Sebastian and I do it.
This change is not a priority for us right now. We will do it, but not now.
This kind of PR rots quickly. So, I am closing it.
I appreciate the attitude. If you want to help, we have many items marked with "help wanted". If one of them is interesting to you, write a note there, and we will work with you to get a PR merged.

[Julian]

Perfectly understandable! Will do.