odd link anchor for “subsingletons”

[nomeata]

The intro text of https://lean-lang.org/doc/reference/latest/The-Type-System/Propositions/#propositions has a link to subsingletons that goes to

https://lean-lang.org/doc/reference/latest/The-Type-System/Inductive-Types/#--tech-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next

which I am not sure is an intended anchor :-)

[david-christiansen]

It's an internal one! But it could indeed be nicer-looking.

I'd like to figure out how to show proper permalinks in the address bar when they exist, but I'm not sure how to do it.