diff --git a/src/ccl/design/mutability.md b/src/ccl/design/mutability.md
index bb6a2baa..36c0bf7c 100644
--- a/src/ccl/design/mutability.md
+++ b/src/ccl/design/mutability.md
@@ -955,11 +955,16 @@ The value-`Case` positions ride the same union-of-restricts:
   constant boolean directly (no new runtime capability).
 - **Data-typed selection** (`zs = xs if c else ys`) — *implemented*
   (`lambda_elim::build_value_case_fanout`): each arm's whole collection restricted by a
-  constant-in-element gate, unioned; the union carries the Σ the type system gave the `Case` (see
-  `design/type-inference.md` §4.6), and the strict wall reconciles its structural `Variant`-domain
-  type against the Σ by **Σ-introduction** (the compiled gated partition realizes the whole sum —
-  the finite-Σ = gated-coproduct iso, legs' base domains set-equal to the candidates), or against
-  the same-domain collapse's plain data fun. `elif` chains flatten to one N-choice
+  constant-in-element gate, then assembled with `DisjointJoin` over the one domain the arms
+  share (see `design/type-inference.md`, "4.6 Data vs compute functions"). The join lands on
+  that domain and carries the type the type system gave the `Case`, so the strict `typecheck`
+  pass has no coproduct claim to undo. Arms at differing domains have no shared domain to land
+  on and inference rejects them, so the fan-out is only built at one domain; `Σ` is the recorded
+  design for the differing case (`design/type-inference.md`, "The domain join is a Σ"), where
+  **Σ-introduction** relates a structural `Variant`-domain type to the Σ — the compiled gated
+  partition realizes the whole sum, by the finite-Σ = gated-coproduct iso with the legs' base
+  domains set-equal to the candidates. `elif`
+  chains flatten to one N-choice
   partition first. A conditional collection is *consumed* (aggregate, program result) via the
   `Σ <: Fun` subtyping rule, and *through a comprehension* by floating the source `Case` out of the
   map (see the comprehension bullet below).
diff --git a/tests/compilation_pipeline/conditionals.rs b/tests/compilation_pipeline/conditionals.rs
index 1dafa928..8c931987 100644
--- a/tests/compilation_pipeline/conditionals.rs
+++ b/tests/compilation_pipeline/conditionals.rs
@@ -191,10 +191,11 @@ fn test_value_ternary_skips_partial_off_path_arm(#[case] code: &str, #[case] exp
 // type system gave the `Case`; exactly one gated arm is non-empty, so consuming
 // the union (here via `sum`) sees just that arm's elements.
 //
-// The union's tagged-`Variant` domain reconciles against the arms' joined data
-// function by `is_index_partition_of`: every leg is that one domain under its own
-// gate. Arms at *distinct* domains have no join to subtype against and are rejected
-// at inference, so the fan-out is only built at one domain.
+// The legs are partial maps over that one domain, kept disjoint by the gates, so
+// the fan-out assembles them with `DisjointJoin` and lands on the domain directly
+// — no coproduct claim for a consumer to undo. Arms at distinct domains have no
+// join to subtype against and are rejected at inference, so the fan-out is only
+// built at one domain.
 // ---------------------------------------------------------------------------
 
 #[rstest]
@@ -227,10 +228,8 @@ sum([10, 20] if n == 1 else [1, 2])",
 )]
 // `elif` over collections — first matching arm's collection wins. **Three legs over
 // one fiber**: the three arms all have domain `[0, 1)`, so the fan-out is a
-// three-leg `Variant` whose payloads are all that one domain under different gates.
-// This is exactly what `is_index_partition_of` must accept — a positional
-// leg↔domain bijection would reject it — and what an `if`/`elif` accumulator write
-// produces.
+// three-leg `DisjointJoin` over that one domain, each leg restricted by its own
+// gate. This is the shape an `if`/`elif` accumulator write produces.
 #[case(
     r"
 n: Int = 1