diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -34,7 +34,7 @@
 
 ```bash
 cabal update
-cabal install --overwrite-policy=always phino-0.0.81
+cabal install --overwrite-policy=always phino-0.0.95
 phino --version
 ```
 
diff --git a/phino.cabal b/phino.cabal
--- a/phino.cabal
+++ b/phino.cabal
@@ -1,6 +1,6 @@
 cabal-version: 3.0
 name: phino
-version: 0.0.95
+version: 0.0.96
 license: MIT
 synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions
 description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
diff --git a/resources/dataization.yaml b/resources/dataization.yaml
--- a/resources/dataization.yaml
+++ b/resources/dataization.yaml
@@ -67,11 +67,14 @@
 - name: none
   match: ⟦𝐵⟧
   e-match: 𝑒
-  d-result: '--'
+  d-result: δ
   when:
     disjoint:
       - [Δ, λ, φ]
       - [𝐵]
+  premises:
+    - d-result: δ
+      dataize: ⊥
 
 - name: end
   match: ⊥
diff --git a/resources/morphing.yaml b/resources/morphing.yaml
--- a/resources/morphing.yaml
+++ b/resources/morphing.yaml
@@ -110,9 +110,15 @@
 - name: xi
   match: ξ
   e-match: 𝑒
-  n-result: ⊥
+  n-result: 𝑛
+  premises:
+    - n-result: 𝑛
+      morph: ⊥
 
 - name: mg
   match: Φ
   e-match: Φ
-  n-result: ⊥
+  n-result: 𝑛
+  premises:
+    - n-result: 𝑛
+      morph: ⊥
diff --git a/resources/normalize/dl.yaml b/resources/normalize/dl.yaml
--- a/resources/normalize/dl.yaml
+++ b/resources/normalize/dl.yaml
@@ -2,13 +2,13 @@
 # SPDX-License-Identifier: MIT
 ---
 name: dl
-pattern: ⟦𝐵⟧
+pattern: ⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧
 result: ⊥
 when:
-  and:
+  or:
     - in:
         - Δ
-        - 𝐵
+        - 𝐵1
     - in:
-        - λ
-        - 𝐵
+        - Δ
+        - 𝐵2
diff --git a/src/Dataize.hs b/src/Dataize.hs
--- a/src/Dataize.hs
+++ b/src/Dataize.hs
@@ -161,7 +161,8 @@
 -- ternary, 𝔻(n, e, s): besides the term 'n' it takes the universe 'e' ('univ'),
 -- which it forwards to 𝕄, and the mutable state 's', returning the bytes together
 -- with the new state. Its rules come from 'dataization.yaml': 'delta' yields the
--- asset bytes, 'none' (a formation) and 'end' (⊥) yield empty bytes (--),
+-- asset bytes, 'end' (⊥) yields empty bytes (--) and 'none' (a formation with no
+-- Δ/λ/φ) delegates to 'end' by dataizing ⊥,
 -- 'box' contextualizes the φ-body and keeps dataizing (its step is labelled by
 -- its 'contextualize' side-computation), and 'norm' reduces through morphing,
 -- splicing the morphing steps into the chain. The clauses are disjoint (see
@@ -215,11 +216,14 @@
           built <- buildExpressionThrows inner final
           ((morphed', seq'), state'') <- morph (built, seq) univ state' ctx
           dataize' (morphed', seq') univ state'' ctx
+        -- 𝔻(⊥) (the 'none' rule) hands a literal term straight to 𝔻 with no
+        -- producing side-computation, so the transition to that term is labelled
+        -- by the conclusion's own verb ('dataize') rather than a side premise.
         _ -> do
           let side = rule.premises `excluding` [concl]
           (final, state') <- sides side subst
           built <- buildExpressionThrows arg final
-          seq' <- leadsTo seq (labelOf side) built ctx
+          seq' <- leadsTo seq (labelOr (verb concl.operation) side) built ctx
           dataize' (built, seq') univ state' ctx
       Just _ -> throwIO (userError (printf "dataization rule '%s' must conclude with a 'dataize' premise" rule.name))
     sides :: [Y.Premise] -> Subst -> IO (Subst, State)
@@ -229,6 +233,11 @@
     labelOf :: [Y.Premise] -> String
     labelOf (premise : _) = verb premise.operation
     labelOf [] = ""
+    -- As 'labelOf', but falls back to the given label when there is no
+    -- side-computation to name the step (the 'none' rule's 𝔻(⊥) premise).
+    labelOr :: String -> [Y.Premise] -> String
+    labelOr _ premises@(_ : _) = labelOf premises
+    labelOr fallback [] = fallback
 
 -- The premise binding the given expression meta, if any. The conclusion of a
 -- morphing rule and the argument of a continuation premise are looked up here to
diff --git a/src/Render.hs b/src/Render.hs
--- a/src/Render.hs
+++ b/src/Render.hs
@@ -273,9 +273,13 @@
   render CO_DISJOINT{..} =
     "[ "
       <> T.intercalate " \\char44{} " (map render attrs)
-      <> " ] \\cap \\lparen "
-      <> T.intercalate " \\cup " (map render groups)
-      <> " \\rparen = \\emptyset"
+      <> " ] \\cap "
+      <> renderGroups groups
+      <> " = \\emptyset"
+    where
+      renderGroups :: [BINDING] -> Text
+      renderGroups [group] = render group
+      renderGroups gs = "\\lparen " <> T.intercalate " \\cup " (map render gs) <> " \\rparen"
   render CO_EMPTY = ""
 
 renderFunc :: Render a => Text -> a -> Text
diff --git a/test/CLISpec.hs b/test/CLISpec.hs
--- a/test/CLISpec.hs
+++ b/test/CLISpec.hs
@@ -1004,9 +1004,9 @@
             , "  { }"
             , "  { }"
             , "\\phinoNormalizationRule{dl}"
-            , "  { [[ B ]] }"
+            , "  { [[ B_1, L> F, B_2 ]] }"
             , "  { T }"
-            , "  { D \\in B \\;\\text{and}\\; L \\in B }"
+            , "  { D \\in B_1 \\;\\text{or}\\; D \\in B_2 }"
             , "  { }"
             , "\\phinoNormalizationRule{dot}"
             , "  { [[ B_1, \\tau -> n, B_2 ]] . \\tau }"
@@ -1097,11 +1097,13 @@
             , "\\end{phinoMorphingInference}"
             , "\\begin{phinoMorphingInference}"
             , "  \\phinoName{xi}"
-            , "  \\phinoConclusion{ \\phinoMorph{ \\phiTerminal{\\xi} }{ e }{ s }{ T }{ s } }"
+            , "  \\phinoPremise{ \\phinoMorph{ T }{ e }{ s_1 }{ n }{ s_2 } }"
+            , "  \\phinoConclusion{ \\phinoMorph{ \\phiTerminal{\\xi} }{ e }{ s_1 }{ n }{ s_2 } }"
             , "\\end{phinoMorphingInference}"
             , "\\begin{phinoMorphingInference}"
             , "  \\phinoName{mg}"
-            , "  \\phinoConclusion{ \\phinoMorph{ Q }{ Q }{ s }{ T }{ s } }"
+            , "  \\phinoPremise{ \\phinoMorph{ T }{ e }{ s_1 }{ n }{ s_2 } }"
+            , "  \\phinoConclusion{ \\phinoMorph{ Q }{ Q }{ s_1 }{ n }{ s_2 } }"
             , "\\end{phinoMorphingInference}"
             ]
         ]
@@ -1132,8 +1134,9 @@
             , "\\end{phinoDataizationInference}"
             , "\\begin{phinoDataizationInference}"
             , "  \\phinoName{none}"
-            , "  \\phinoCondition{ [ D \\char44{} L \\char44{} @ ] \\cap \\lparen B \\rparen = \\emptyset }"
-            , "  \\phinoConclusion{ \\phinoDataize{ [[ B ]] }{ e }{ s }{ |--| }{ s } }"
+            , "  \\phinoCondition{ [ D \\char44{} L \\char44{} @ ] \\cap B = \\emptyset }"
+            , "  \\phinoPremise{ \\phinoDataize{ T }{ e }{ s_1 }{ \\delta }{ s_2 } }"
+            , "  \\phinoConclusion{ \\phinoDataize{ [[ B ]] }{ e }{ s_1 }{ \\delta }{ s_2 } }"
             , "\\end{phinoDataizationInference}"
             , "\\begin{phinoDataizationInference}"
             , "  \\phinoName{end}"
diff --git a/test/DataizeSpec.hs b/test/DataizeSpec.hs
--- a/test/DataizeSpec.hs
+++ b/test/DataizeSpec.hs
@@ -261,6 +261,12 @@
     it "dataizes a located reference through the expected rules" $ do
       labels <- labelsOf "Q.foo.bar" "Q -> [[ foo -> [[ bar -> [[ @ -> Q.x ]] ]], x -> [[ D> 42- ]] ]]"
       labels `shouldBe` ["contextualize", "md", "dot", "copy", "mf"]
+    -- The 'none' rule no longer emits '--' itself: it delegates to 'end' by
+    -- dataizing ⊥, so the empty formation reduces through one labelled 'dataize'
+    -- step (𝔻(⟦⟧) → 𝔻(⊥)) before 'end' yields the empty bytes (#942).
+    it "dataizes an empty formation by delegating to end" $ do
+      labels <- labelsOf "Q" "Q -> [[ ]]"
+      labels `shouldBe` ["dataize"]
 
   testDataize
     [