Use the state set notation of state errors in hints and declared-here #515

Problem

Since #511, the headline of a state error prints the states of named sets as values of their sets, but the hints and "declared here" do not. One message now uses three notations for the same states. Real output on main (0.0.37) for ErrorStateHintMultipleSets (sets doorState, lockState):

State Refinement Error: found doorState(d@26) == closed && lockState(d) == locked && doorState(d) == doorState(d@26) but expected doorState(d) == closed && lockState(d) == unlocked
28 |         d.open();
Hints:
  - Call d.unlock() before this call to move d from locked to unlocked
  - In state closed and locked, d can call: unlock()

--> Refinement declared here:
13 |     @StateRefinement(from = "closed(this) && unlocked(this)", to = "opened(this)")

The headline says lockState(d) == locked, the hints say locked, and "declared here" says closed(this). A first-time reader has to work out on their own that these are the same thing. A UX review and a verification review agreed that this is the main regression of the named-set change. In the study it would be confounded with the change itself. Hint state lists also have no grouping: In state undoable and notRedoable or notUndoable and notRedoable, ....

Proposal (display only, named sets only; unnamed sets keep the shorthand, as in #511)

1. Hints name the set of each state of a named set, matching the headline. For example:

   • Call d.unlock() before this call to move lockState of d from locked to unlocked
   • In state doorState == closed and lockState == locked, d can call: unlock()

   The exact wording is open. The constraint is that the hint reads as the same notation as the headline.

2. Group the alternatives in hint state lists, so and/or cannot be misread. For example: In state (undoable and notRedoable) or (notUndoable and notRedoable), or, better, only the set that matters.

3. "Declared here" stays verbatim (it is source). When it uses the shorthand for states of named sets, add one gloss line under it: closed means doorState == closed, unlocked means lockState == unlocked. Only the states that appear in the excerpt.

4. Check how the VS Code extension shows hints and the declared-here excerpt. If the gloss needs an extension change, open a follow-up issue on vscode-liquidjava instead of doing it here.

Nothing the verifier decides changes: not the VC, the verdict, which hints are given, or the category.

Tests

Update the exact-message tests in TestStateHints that already cover named sets (e.g. foundKeepsANamedStateSetByItsName), plus a few focused tests that fail without the change.