clean up prose and remove out-of-place comment on POOL-reg.

Author: williamdemeo

src/Ledger/Dijkstra/Specification/Certs.lagda.md

@@ -394,11 +394,7 @@ coinFromDeposits cs =
 ```
 
 A `CertState`{.AgdaRecord} is *pool-deposit registered* when every entry of the pool
-deposit pot belongs to a registered pool.  Deposit accounting relies on this:
-`POOL-reg`{.AgdaInductiveConstructor} adds the pool deposit with a left-biased union,
-so a stale pot entry for an unregistered pool would silently swallow the added
-deposit.  The property is preserved by `CERTS`{.AgdaDatatype} (both maps gain exactly
-the new pool's key, and no rule removes a pool without its deposit).
+deposit pot belongs to a registered pool.
 
 ```agda
 PoolDepositsRegistered : CertState → Type