Update the value-Case fan-out's prose to the DisjointJoin it builds

[dpmills]

Three prose sites still described the value-Case fan-out as it worked before the CollectionUnion split (#86), reconciling a coproduct against the Case's type by is_index_partition_of — a helper #86 deleted. Two are test comments, one is mutability.md's data-typed-selection bullet; all three now state what lambda_elim::build_value_case_fanout builds, a DisjointJoin over the one domain the arms share. Σ stays as the recorded design for arms at differing domains, which inference rejects today. Comments and doc prose only, no code changes.

[dpmills]

This change is part of the following stack:

• Freshening asks a different question than type_level, so it needs its own #71
  • SharedHole: let lowering state that two type positions are the same #72
    • Traits: state what an operator requires of its operands, not that they are the same #73
      • Mutable-variable typing: an honest seed, a fixed history read-through, and a polarity-directed base #52
        • Annotations stop standing in for binder structure, and stop outliving inference #60
          • Four defects in how Mut is typed: message polarity, an unclosable refinement, and op= as a rebind #63
            • A mutable variable read is an explicit operation, not a subtyping rule #64
              • Exact and bounded binder annotations: x: T fixes the type, x <: T bounds it #62
                • constrain_go asserts the uniquely-keyed invariant it rests on #74
                  • Update the value-Case fan-out's prose to the DisjointJoin it builds #75 ◀
                  • Canonicalize each arrow's Pi binder as the solver flattens types #76
                  • Hold a refined type's refinements in one unordered set instead of nested layers #77
                  • Derive a Cast's refinements from its term instead of overwriting the target #78
                  • Add a Lean model of the CCL type system and fuzz the solver against it #79

_{Change managed by git-spice.}

[sortalongo]

Can you do a redundant-jargon pass? There are a few terms that I hadn't seen before cropping up here that I'm not sure deserve coining (grounded subtyping, gate, bridge, chain).

[dpmills]

After rebasing, this was actually made obsolete by PR 86. There was a bit of related cleanup to do, so I've done those tiny changes here