Highlight data should distinguish bindings even in case of state rollback

Currently, when an example contains an error or when the user asks for it, we roll back the elaborator state after an example.

This is generally the right thing, but it has one downside: the unique variable counter gets reset, and later elaborator runs might re-use internal IDs. This can lead to mistaken extra highlights:

There should be some way of preventing this, e.g. by postprocessing the elaborated example to extract the highest ID, then bumping the counter.

Start by tracing how elaborator state rollback resets the unique variable counter after an example, then reproduce the mistaken extra highlights shown in the issue. The work is done when later elaborator runs cannot reuse internal IDs after rollback and the extra highlights no longer appear.