diff --git a/design/mvp/Binary.md b/design/mvp/Binary.md
index 9a82702a..4e3a8d32 100644
--- a/design/mvp/Binary.md
+++ b/design/mvp/Binary.md
@@ -251,7 +251,8 @@ Notes:
 * All parameter labels, result labels, record field labels, variant case
   labels, flag labels, enum case labels, component import names, component
   export names, instance import names and instance export names must be
-  unique in their containing scope.
+  unique in their containing scope, considering two labels that differ only in
+  case to be equal and thus rejected.
 * Validation of `externdesc` requires the various `typeidx` type constructors
   to match the preceding `sort`.
 * (The `0x00` immediate of `case` may be reinterpreted in the future as the
diff --git a/design/mvp/Explainer.md b/design/mvp/Explainer.md
index aabc221e..0247774e 100644
--- a/design/mvp/Explainer.md
+++ b/design/mvp/Explainer.md
@@ -1562,6 +1562,12 @@ mapped to `isXML`, `IsXml`, `is_XML` or `is_xml`, depending on the target
 language/convention. The highly-restricted character set ensures that
 capitalization is trivial and does not require consulting Unicode tables.
 
+Because some casing schemes (such as all-lowercase) would lead to clashes if
+two `label`s differed only in case, in all cases where "uniquness" is required
+between a set of names (viz., import/export names, record field labels, variant
+case labels, and function parameter/result names), two `label`s that differ
+only in case are considered equal and thus rejected.
+
 Components provide two options for naming exports, symmetric to the first two
 options for naming imports:
 * a **plain name** that leaves it up to the developer to "read the docs"
diff --git a/design/mvp/WIT.md b/design/mvp/WIT.md
index e0d09db2..005d8671 100644
--- a/design/mvp/WIT.md
+++ b/design/mvp/WIT.md
@@ -234,9 +234,10 @@ world command {
 }
 ```
 
-Kebab names cannot overlap and must be unique, even between imports and exports.
-IDs, however, can be both imported and exported. The same interface cannot be
-explicitly imported or exported twice.
+Each name must be case-insensitively unique in the scope in which it is
+declared. In the case of worlds, all imported names are in the same scope,
+but separate from all the export names, and thus the same name can *not* be
+imported twice, but *can* be both imported and exported.
 
 [Plain Name]: Explainer.md#import-and-export-definitions
 
@@ -647,7 +648,7 @@ import unless it's explicitly listed as an export.
 
 Functions are defined in an [`interface`][interfaces] or are listed as an
 `import` or `export` from a [`world`][worlds]. Parameters to a function must all
-be named and have unique names:
+be named and have case-insensitively unique names:
 
 ```wit
 package local:demo;