feat: make declaration-keyed extension entries write-once

This PR makes entries of declaration-keyed environment extensions write-once: writing a second entry for a declaration panics, and giving a declaration a second docstring through `add_decl_doc` is an error. A failed redeclaration also no longer replaces the declaration ranges of the existing declaration, which misdirected go-to-definition. Apart from catching accidental overwrites, this is a necessary prerequisite for validating type class resolution cache entries against declaration-keyed registries, such as equation theorems, without recording every read of them.

`MapDeclarationExtension.insert` takes an `allowOverwrite` flag for deliberate replacements; no caller in core needs it. Its guard only serves to catch bugs, as the type class resolution cache will record writes through `insert`; the registries below are not recorded, so there the cache will rely on the guard. `addDeclarationRanges` keeps the first ranges reported for a declaration, and docstrings otherwise still replace an existing one, as metaprograms such as cross-reference attributes write them before a declaration's own docstring is added. The declaration-keyed registries kept in other extensions (structures, equation theorems, match equations, sparse `casesOn` declarations, definition height overrides) get the same guard, allowing idempotent re-registration; `setStructureParents` remains the one sanctioned update of a structure's entry. A rejected write keeps the existing entries, and the checks only consult the state visible on the current environment branch, so that a write never waits for the branch elaborating the declaration.

The guard caught docstrings in the standard library that were silently replaced: `add_decl_doc IterM.mk` after `structure Iter` meant `Iter.mk`, and `WellFounded.extrinsicFix`, its variants, `IterM.Total` and `Iter.Total` had placeholder docstrings, kept only to satisfy the missing-docs linter, that a later `add_decl_doc` referring to subsequent declarations replaced. These now opt out of the linter instead.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>