Universe variables shown confusingly in example

From Zulip:

There are universe inconsistencies in the two examples in section 2.4. In the "Equational Lemmas" example we're shown some code with no universes mentioned, and the equational lemmas are peppered with references to universe u_1, except for thirdOfFive.eq_1 which is all about universe u. (except for when you hover, in which case you see u_1 again). Conversely the other example, "Recursive Equational Lemmas", again is a discussion about code written where no universes are mentioned, but all the equation lemmas use universe u consistently in the text (although all hovers talk about universe u_1). I don't know if this is confusing for new users, I guess my instinct is to make it consistent (and consistency within the first example would surely be desirable rather than thirdOfFive.eq_1 being the odd one out).

This should be fixed. It will require a bit of attention to the delaboration and pretty printing that gives rise to hovers.

Start with the two examples in section 2.4, “Equational Lemmas” and “Recursive Equational Lemmas,” and compare their displayed universe variables with the hover information. Then inspect the delaboration and pretty printing that produce these displays. Done means the universe naming is consistent within and between the examples, including thirdOfFive.eq_1.