docs: add ToCs + clear obsolete SPDX-normalization follow-up note

- README.md: manual markdown Contents section after the badges block,
  mirroring the Axiom.jl-style top-of-file ToC pattern
- readme.adoc: `:toc:` + `:toclevels: 2` macros
- EXPLAINME.adoc: `:toc:` + `:toclevels: 2` macros (was missing — the
  other audience-facing .adoc files already had :toc:)
- README.md + readme.adoc: drop the "current practical follow-up"
  licensing bullet (the SPDX-header normalization it referenced just
  landed in PR #150, so the line is now obsolete) and tighten the
  remaining bullets from "intended to be licensed" -> "licensed"

QUICKSTART-DEV.adoc / QUICKSTART-MAINTAINER.adoc / QUICKSTART-USER.adoc /
INDEX.adoc / TOPOLOGY.adoc already carry `:toc:` so are unchanged.

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

Author: hyperpolymath

EXPLAINME.adoc

@@ -1,6 +1,8 @@
 // SPDX-License-Identifier: MPL-2.0
 = echo-types: explain me
 :icons: font
+:toc:
+:toclevels: 2
 
 == One paragraph
 

README.md

@@ -15,6 +15,27 @@ Constructive Agda development for echo types as a first-class notion of structur
 
 loss that is not total erasure.
 
+## Contents
+
+- [Where things are](#️-where-things-are)
+- [Structural overview](#-structural-overview)
+- [Recommended reading order](#-recommended-reading-order)
+- [Core Idea](#core-idea)
+- [Definition (Foundation)](#definition-foundation)
+- [Canonical identity layer (2026-05-27)](#canonical-identity-layer-2026-05-27)
+- [Current Status Snapshot](#current-status-snapshot)
+  - [Echo Core (load-bearing for the identity claim)](#echo-core-load-bearing-for-the-identity-claim)
+  - [Ordinal / Buchholz (parallel-independent, experimental)](#ordinal--buchholz-parallel-independent-experimental)
+- [External Bridge Targets (local workspace)](#external-bridge-targets-local-workspace)
+- [What Echo Types Are For](#what-echo-types-are-for)
+- [Identity Claim and Falsifiability](#identity-claim-and-falsifiability)
+- [Build](#build)
+  - [Installing as a library](#installing-as-a-library)
+- [Citation](#citation)
+- [Tooling Stance](#tooling-stance)
+- [Roadmap](#roadmap)
+- [Licensing](#licensing)
+
 ## 🗺️ Where things are
 
 **New here, or can't find something? Start with the
@@ -446,6 +467,5 @@ into `roadmap.adoc` and removed.
 
 ## Licensing
 
-- code, proofs, and tooling in this repository are intended to be licensed under `MPL-2.0`; see [LICENSE](LICENSE)
-- prose documentation in `docs/`, `README.md`, `readme.adoc`, and roadmap files is intended to be licensed under `CC-BY-4.0`; see [LICENSE-docs](LICENSE-docs)
-- current practical follow-up: normalize per-file SPDX headers across source files so file-level notices match the top-level licensing intent
+- code, proofs, and tooling in this repository are licensed under `MPL-2.0`; see [LICENSE](LICENSE)
+- prose documentation in `docs/`, `README.md`, `readme.adoc`, and roadmap files is licensed under `CC-BY-4.0`; see [LICENSE-docs](LICENSE-docs)

readme.adoc

@@ -1,4 +1,6 @@
 = echo-types
+:toc:
+:toclevels: 2
 
 image::docs/assets/banner.png[Echo Types — Proof-Relevant Information Residues,align="center"]
 
@@ -282,6 +284,5 @@ Open/gated work and cross-repo follow-ups are tracked in:
 
 == Licensing
 
-* code, proofs, and tooling in this repository are intended to be licensed under `MPL-2.0`; see `LICENSE`
-* prose documentation in `docs/`, `README.md`, `readme.adoc`, and roadmap files is intended to be licensed under `CC-BY-4.0`; see `LICENSE-docs`
-* practical follow-up: normalize per-file SPDX headers across source files so file-level notices match the top-level licensing intent
+* code, proofs, and tooling in this repository are licensed under `MPL-2.0`; see `LICENSE`
+* prose documentation in `docs/`, `README.md`, `readme.adoc`, and roadmap files is licensed under `CC-BY-4.0`; see `LICENSE-docs`