Consolidate HKTBs, leak-check and universes information around with what we have in the guide

[spastorino]

There's great information about all these concepts in MCPs, PRs, issues, etc.

• Universes #55517
• Tracking issue for "universe transition" #56105
• Re-implement leak check in terms of universes #58592
• eventual goal: re-remove leak-check from compiler #59490
• replace the leak check with universes, take 2 #65232
• extend NLL checker to understand 'empty combined with universes #70950
• MCP: move leak-check to during coherence, candidate eval
• move leak-check to during coherence, candidate eval #72493
• the existing HRTB page in the guide, which mentions what are placeholder leaks, some information about the leak check, and so on but it seems to describe the state of things pre-universes and they have changed since then (as shown in the list of PRs above)

Would be great to review them and add stuff into the guide.

[spastorino]

#374 is related.