diff --git a/crates/ailang-prose/src/lib.rs b/crates/ailang-prose/src/lib.rs
index 7d6f110..47eed72 100644
--- a/crates/ailang-prose/src/lib.rs
+++ b/crates/ailang-prose/src/lib.rs
@@ -54,11 +54,11 @@ fn write_module(out: &mut String, m: &Module) {
         }
     }
 
-    // Ct.4.3: the file's own module name is the owner-qualifier that
-    // the prose surface trims when it appears on intra-module
-    // `Type::Con.name`. Cross-module qualifiers (any other owner)
-    // round-trip verbatim. Threaded through every recursive write_*
-    // that can reach a `Type::Con`.
+    // The file's own module name is the owner-qualifier that the
+    // prose surface trims when it appears on intra-module
+    // `Type::Con.name`. Cross-module qualifiers round-trip verbatim.
+    // Threaded through every recursive write_* that can reach a
+    // `Type::Con`.
     let owning_module = m.name.as_str();
 
     for def in &m.defs {
@@ -470,12 +470,11 @@ fn write_type(out: &mut String, t: &Type, owning_module: &str) {
     match t {
         Type::Var { name } => out.push_str(name),
         Type::Con { name, args } => {
-            // Ct.4.3: trim a qualifier whose owner matches the current
-            // file's module: `prelude.Ordering` printed from inside
-            // `prelude` becomes bare `Ordering`. Cross-module qualifiers
-            // (any other owner) survive verbatim. Mirrors the post-ct.1
-            // canonical-form rule "bare = local, qualified = cross-
-            // module" on the prose surface.
+            // Trim a qualifier whose owner matches the current file's
+            // module: `prelude.Ordering` printed from inside `prelude`
+            // becomes bare `Ordering`. Cross-module qualifiers survive
+            // verbatim. Mirrors the canonical-form rule "bare = local,
+            // qualified = cross-module" on the prose surface.
             let display_name = match name.split_once('.') {
                 Some((owner, suffix)) if owner == owning_module => suffix,
                 _ => name.as_str(),
@@ -800,12 +799,12 @@ fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8, ow
             ctor,
             args,
         } => {
-            // Ct.4.3: the Ctor `type_name` field is intentionally
-            // elided from the prose surface — the type is recoverable
-            // from typecheck context, and showing it on every Ctor
-            // would clutter the read. The qualifier-trim that applies
-            // to `Type::Con.name` therefore has no analogue here:
-            // there is no `out.push_str(type_name)` site to trim.
+            // The Ctor `type_name` field is intentionally elided from
+            // the prose surface — the type is recoverable from
+            // typecheck context, and showing it on every Ctor would
+            // clutter the read. The qualifier-trim that applies to
+            // `Type::Con.name` therefore has no analogue here: there
+            // is no `out.push_str(type_name)` site to trim.
             out.push_str(ctor);
             if !args.is_empty() {
                 out.push('(');