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.104
+version: 0.0.105
 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
@@ -15,11 +15,11 @@
 # to one judgment — 𝔻 ('dataize'), 𝕄 ('morph'), 𝒩 ('normalize'), 𝔼 ('evaluate')
 # or 𝒞 ('contextualize'). 'e-match' is the universe-argument matcher of
 # 𝔻(n, e); it is always the e meta. The single bytes result is named δ. A
-# normal-form-valued result (𝕄 'morph', 𝒩 'normalize') is named 𝑛, 𝑛1, … in
-# premise order, skipping the bare 𝑛 only when 'match' already binds it; an
-# expression-valued result (𝒞 'contextualize', 𝔼 'evaluate') is not a normal
-# form — that is why a 'normalize' premise follows it — so it takes an 𝑒-family
-# name (𝑒1, 𝑒2, …, the next index free of 'match', 𝑒 itself being the universe)
+# normal-form-valued result (𝕄 'morph', 𝒩 'normalize', 𝔼 'evaluate') is named
+# 𝑛, 𝑛1, … in premise order, skipping the bare 𝑛 only when 'match' already binds
+# it; an expression-valued result (𝒞 'contextualize') is not a normal form —
+# that is why a 'normalize' premise follows it — so it takes an 𝑒-family name
+# (𝑒1, 𝑒2, …, the next index free of 'match', 𝑒 itself being the universe)
 # rather than an 𝑛 name reserved for normal forms.
 #
 # The clauses are disjoint, so their relative order does not change behavior.
@@ -61,12 +61,10 @@
   e-match: 𝑒
   d-result: δ
   premises:
-    - n-result: 𝑒1
+    - n-result: 𝑛1
       evaluate:
         - ⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧
         - 𝑒
-    - n-result: 𝑛1
-      normalize: 𝑒1
     - d-result: δ
       dataize: 𝑛1
 
diff --git a/resources/morphing.yaml b/resources/morphing.yaml
--- a/resources/morphing.yaml
+++ b/resources/morphing.yaml
@@ -19,12 +19,11 @@
 # ordered 'premises' reduce as stated. A premise binds 'n-result' to the result
 # of one judgment — 𝕄 ('morph'), 𝒩 ('normalize') or 𝔼 ('evaluate'). 'e-match' is
 # the universe-argument matcher of 𝕄(n, e); usually the e meta, but a rule may
-# pin it to a literal (e.g. 'mg' fires only on 𝕄(Φ, Φ)). A normal-form-valued
-# result (𝕄 'morph', 𝒩 'normalize') is named 𝑛, 𝑛1, … in premise order, the bare
-# 𝑛 skipped only when 'match' already binds it; an expression-valued result (𝔼
-# 'evaluate') is not a normal form — that is why a 'normalize' premise follows
-# it — so it takes an 𝑒-family name (𝑒1, 𝑒2, …, the next index free of 'match',
-# 𝑒 itself being the universe) rather than an 𝑛 name reserved for normal forms.
+# pin it to a literal (e.g. 'mg' fires only on 𝕄(Φ, Φ)). Every judgment here is
+# normal-form-valued (𝕄 'morph', 𝒩 'normalize', 𝔼 'evaluate' — 𝔼 normalizes its
+# atom's result internally), so results are named 𝑛, 𝑛1, … in premise order, the
+# bare 𝑛 skipped only when 'match' already binds it; the 𝑒-family stays reserved
+# for the universe 𝑒 itself.
 #
 # 'ml' and 'md' are kept mutually exclusive: 'md' fires only
 # when its head 𝑛 is not a formation ('not (formation 𝑛)'), so every formation
@@ -55,19 +54,19 @@
   label: \lambda
   match: '⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧.𝜏'
   e-match: 𝑒
-  n-result: 𝑛2
+  n-result: 𝑛3
   premises:
-    - n-result: 𝑒1
+    - n-result: 𝑛1
       evaluate:
         - '⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧'
         - 𝑒
-    - n-result: 𝑛1
-      normalize: '𝑒1.𝜏'
     - n-result: 𝑛2
-      morph: 𝑛1
+      normalize: '𝑛1.𝜏'
+    - n-result: 𝑛3
+      morph: 𝑛2
 
 - name: mphi
-  label: \phi
+  label: \varphi
   match: ⟦𝐵⟧.𝜏
   e-match: 𝑒
   n-result: 𝑛1
diff --git a/src/AST.hs b/src/AST.hs
--- a/src/AST.hs
+++ b/src/AST.hs
@@ -26,6 +26,13 @@
   | ExMeta Text
   | ExPhiMeet (Maybe String) Int Expression
   | ExPhiAgain (Maybe String) Int Expression
+  | {- | Bare data 𝛿 — the raw bytes extracted by the 'delta' dataization rule.
+    It is not a phi-calculus term but a rendering-only chain node, so a
+    '--sequence' derivation can terminate at the data itself rather than at
+    the data object it was pulled out of (see #980). It never flows into the
+    matcher, builder or the dataization relation.
+    -}
+    ExBytes Bytes
   deriving (Eq, Ord, Show, Generic)
 
 data Argument
@@ -110,6 +117,7 @@
       ExMeta t -> hashText (step h 7) t
       ExPhiMeet ms i ex -> goExpr (hashMaybeString (step (step h 9) i) ms) ex
       ExPhiAgain ms i ex -> goExpr (hashMaybeString (step (step h 10) i) ms) ex
+      ExBytes bts -> goBytes (step h 8) bts
     goBinding :: Int -> Binding -> Int
     goBinding h = \case
       BiTau at ex -> goExpr (goAttribute (step h 11) at) ex
diff --git a/src/CLI/Parsers.hs b/src/CLI/Parsers.hs
--- a/src/CLI/Parsers.hs
+++ b/src/CLI/Parsers.hs
@@ -122,7 +122,7 @@
 optSequence = switch (long "sequence" <> help "Result output contains all intermediate 𝜑-expressions concatenated with EOL")
 
 optCanonize :: Parser Bool
-optCanonize = switch (long "canonize" <> help "Rename all functions attached to λ binding with F1, F2, etc.")
+optCanonize = switch (long "canonize" <> help "Rename all functions attached to λ binding with Fn1, Fn2, etc.")
 
 optExpression :: Parser (Maybe String)
 optExpression = optional (strOption (long "expression" <> metavar "NAME" <> help "Name for 'phiExpression' element when rendering to LaTeX (see --output option)"))
diff --git a/src/CST.hs b/src/CST.hs
--- a/src/CST.hs
+++ b/src/CST.hs
@@ -177,6 +177,7 @@
   | EX_META {meta :: META}
   | EX_PHI_MEET {prefix :: Maybe String, idx :: Int, expr :: EXPRESSION}
   | EX_PHI_AGAIN {prefix :: Maybe String, idx :: Int, expr :: EXPRESSION}
+  | EX_BYTES {bytes :: BYTES} -- bare data 𝛿, a rendering-only terminal chain node (see #980)
   deriving (Eq, Show)
 
 data ATTRIBUTE
@@ -251,6 +252,14 @@
 expressionToCST :: Expression -> EXPRESSION
 expressionToCST = toCST'
 
+-- Like 'expressionToCST', but lays the expression out from a given base tab
+-- instead of column 0. Used when an expression sits on an already-indented
+-- line (e.g. a '\leadsto' continuation step in the LaTeX --sequence output),
+-- so its wrapped member lines nest one level below that line and its closing
+-- bracket aligns with the opening one.
+expressionToCSTFrom :: Int -> Expression -> EXPRESSION
+expressionToCSTFrom tabs expr = toCST expr (tabs, EOL)
+
 -- A number can be rendered with the sweet numeric literal only when it is
 -- finite. NaN and the infinities have no such literal — and the bare `show`
 -- tokens (`NaN`, `Infinity`, `-Infinity`) would collide with object/function
@@ -310,6 +319,7 @@
   toCST ExXi _ = EX_XI XI
   toCST (ExMeta mt) _ = EX_META (META NO_EXCL (exMetaHead mt) (metaTail mt))
   toCST ExTermination _ = EX_TERMINATION DEAD
+  toCST (ExBytes bts) ctx = EX_BYTES (toCST bts ctx)
   toCST (ExPhiMeet prefix idx expr) ctx = EX_PHI_MEET prefix idx (toCST expr ctx)
   toCST (ExPhiAgain prefix idx expr) ctx = EX_PHI_AGAIN prefix idx (toCST expr ctx)
   toCST (ExFormation [BiVoid AtRho]) ctx = toCST (ExFormation []) ctx
diff --git a/src/Canonizer.hs b/src/Canonizer.hs
--- a/src/Canonizer.hs
+++ b/src/Canonizer.hs
@@ -1,9 +1,9 @@
 -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 -- SPDX-License-Identifier: MIT
 
--- Canonization is the process of replacing function names attrached to
--- lambda bindings with numbered identifiers started from 'F'
--- like 'F1', 'F2', etc.
+-- Canonization is the process of replacing function names attached to
+-- lambda bindings with numbered identifiers prefixed with 'Fn'
+-- like 'Fn1', 'Fn2', etc.
 module Canonizer (canonize, canonizeExpr) where
 
 import AST
@@ -14,7 +14,7 @@
 canonizeBindings [] idx = ([], idx)
 canonizeBindings ((BiLambda (Function _)) : rest) idx =
   let (bds', idx') = canonizeBindings rest (idx + 1)
-   in (BiLambda (Function (T.pack ('F' : show idx))) : bds', idx')
+   in (BiLambda (Function (T.pack ("Fn" <> show idx))) : bds', idx')
 canonizeBindings (BiTau attr expr : rest) idx =
   let (expr', idx') = canonizeExpression expr idx
       (bds', idx'') = canonizeBindings rest idx'
@@ -50,7 +50,7 @@
   let (expr', idx') = canonizeExpression expr idx
    in (ArAlpha alpha expr', idx')
 
--- Canonize a single expression, restarting the 'F' counter from 1 so the
+-- Canonize a single expression, restarting the 'Fn' counter from 1 so the
 -- numbering is local to that expression.
 canonizeExpr :: Expression -> Expression
 canonizeExpr expr = fst (canonizeExpression expr 1)
diff --git a/src/Dataize.hs b/src/Dataize.hs
--- a/src/Dataize.hs
+++ b/src/Dataize.hs
@@ -208,11 +208,12 @@
       Nothing -> do
         (final, state') <- sides rule.premises subst
         bts <- buildBytesThrows rule.dresult final
-        pure ((bts, NE.toList seq), state')
+        seq' <- leadsTo seq rule.name (ExBytes bts) ctx
+        pure ((bts, NE.toList seq'), state')
       Just concl@(Y.Premise _ (Y.OpDataize arg)) -> case producer arg rule.premises of
-        -- 𝔻(𝒩(e)) records the producing step (the 'box' contextualization or the
-        -- 'fire' λ-application), then normalizes its result back to a normal form
-        -- before dataizing on, so 𝔻 only ever sees normal forms.
+        -- 𝔻(𝒩(e)) records the producing step (the 'box' contextualization),
+        -- then normalizes its result back to a normal form before dataizing on,
+        -- so 𝔻 only ever sees normal forms.
         Just normal@(Y.Premise _ (Y.OpNormalize inner)) -> do
           let side = rule.premises `excluding` [concl, normal]
           (final, state') <- sides side subst
@@ -227,9 +228,12 @@
           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.
+        -- The dataize argument is produced with no 'normalize'/'morph' spine to
+        -- splice: 'fire' by its 'evaluate' side-computation (𝔼 now yields a
+        -- normal form itself, so no follow-up 'normalize' is needed) and 'none'
+        -- by handing the literal ⊥ straight to 𝔻. The transition is labelled by
+        -- the side-computation ('evaluate') when there is one, else by the
+        -- conclusion's own verb ('dataize' for 𝔻(⊥)).
         _ -> do
           let side = rule.premises `excluding` [concl]
           (final, state') <- sides side subst
@@ -401,10 +405,12 @@
 execBuildTerm _ ctx func = _buildTerm ctx func
 
 -- The Evaluation function 𝔼(b, e, s): it fires the λ atom of a formation 'b'
--- against the global universe 'e', under the incoming state 𝑠, and returns the
--- atom's result together with the new state. The universe is now passed
--- explicitly as the second argument (rather than threaded behind the scenes),
--- matching how the morphing 𝕄 and dataization 𝔻 functions carry it.
+-- against the global universe 'e', under the incoming state 𝑠, normalizes the
+-- atom's raw result 𝒩(e₁) = n, and returns that normal form together with the
+-- new state. Normalizing here makes 𝔼's codomain 𝓝 (as its type demands), so
+-- callers ('fire', 'ml') need no follow-up 'normalize' premise. The universe is
+-- passed explicitly as the second argument (rather than threaded behind the
+-- scenes), matching how the morphing 𝕄 and dataization 𝔻 functions carry it.
 _evaluate :: DataizeContext -> State -> BuildTermMethodS
 _evaluate ctx state [ArgExpression expr, ArgExpression universe] subst = do
   form <- buildExpressionThrows expr subst
@@ -413,7 +419,9 @@
     ExFormation bds -> do
       resolved <- formation bds univ state ctx
       case resolved of
-        Just (obj, state') -> pure (TeExpression obj, state')
+        Just (obj, state') -> do
+          (normal, _) <- normalized obj ((univ, Nothing) :| []) ctx
+          pure (TeExpression normal, state')
         Nothing -> throwIO (userError "Function evaluate() expects a formation with a λ binding")
     _ -> throwIO (userError "Function evaluate() expects a formation")
 _evaluate _ _ _ _ = throwIO (userError "Function evaluate() requires exactly 2 expression arguments")
diff --git a/src/LaTeX.hs b/src/LaTeX.hs
--- a/src/LaTeX.hs
+++ b/src/LaTeX.hs
@@ -153,17 +153,27 @@
     , maybe "" (printf "\\phiExpression{%s} ") _expression
     ]
 
-body :: [(a, Maybe String)] -> (a -> String) -> String
+-- Join the rendered steps with '\leadsto'. Every step after the first carries
+-- the two-space '\leadsto' indent, so it is rendered from base tab 1 rather
+-- than 0 (via 'baseTab'); this keeps a wrapped multi-line step's members nested
+-- one level below its '\leadsto [[' line and its closing bracket aligned with
+-- that line. The first step has no '\leadsto' prefix and stays at base tab 0.
+body :: [(a, Maybe String)] -> (Int -> a -> String) -> String
 body printed toLatex =
   intercalate
     "\n  \\leadsto "
-    ( map
-        ( \(item, maybeName) ->
-            let item' = toLatex item
+    ( zipWith
+        ( \idx (item, maybeName) ->
+            let item' = toLatex (baseTab idx) item
              in maybe item' (printf "%s \\leadsto_{\\nameref{r:%s}}" item') maybeName
         )
+        [0 ..]
         printed
     )
+  where
+    baseTab :: Int -> Int
+    baseTab 0 = 0
+    baseTab _ = 1
 
 ending :: Bool -> LatexContext -> String
 ending True ctx = printf " \\leadsto\n  \\leadsto \\dots\n\\end{%s}" (phiquation ctx)
@@ -202,7 +212,7 @@
   pure
     ( concat
         [ preamble ctx
-        , body (canonizedRewrittens (compressedRewrittens rewrittens ctx) ctx) (\expr -> renderToLatex (expressionToCST expr) ctx)
+        , body (canonizedRewrittens (compressedRewrittens rewrittens ctx) ctx) (\tabs expr -> renderToLatex (expressionToCSTFrom tabs expr) ctx)
         , ending exceeded ctx
         ]
     )
@@ -212,7 +222,7 @@
   pure
     ( concat
         [ preamble ctx
-        , body (zip (canonizedExpressions (compressedExpressions focused ctx) ctx) rules) (\expr -> renderToLatex (expressionToCST expr) ctx)
+        , body (zip (canonizedExpressions (compressedExpressions focused ctx) ctx) rules) (\tabs expr -> renderToLatex (expressionToCSTFrom tabs expr) ctx)
         , ending exceeded ctx
         ]
     )
@@ -240,6 +250,7 @@
   toLaTeX EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toLaTeX expr)
   toLaTeX EX_META{..} = EX_META (toLaTeX meta)
   toLaTeX EX_XI{} = EX_XI XI'
+  toLaTeX EX_BYTES{..} = EX_BYTES (toLaTeX bytes)
   toLaTeX expr = expr
 
 instance ToLaTeX ATTRIBUTE where
@@ -392,7 +403,7 @@
     premises
     (phinoMorph (renderExpr rule.match) (renderExpr rule.ematch) (conclusionStateName final 1) (conclusionStateName final final) (renderExpr rule.nresult))
   where
-    (premises, final) = premisesToLatex rule.premises
+    (premises, final) = premisesToLatex (renderExpr rule.ematch) rule.premises
 
 -- Render a dataization rule as a LaTeX inference rule, with 𝔻(match, e, s_1) ⟿
 -- ⟨d-result, s_k⟩ as the conclusion below the line, s_k being the final threaded
@@ -407,7 +418,7 @@
     premises
     (phinoDataize (renderExpr rule.match) (renderExpr rule.ematch) (conclusionStateName final 1) (conclusionStateName final final) (renderBytes rule.dresult))
   where
-    (premises, final) = premisesToLatex rule.premises
+    (premises, final) = premisesToLatex (renderExpr rule.ematch) rule.premises
 
 -- Render a contextualization rule as a LaTeX inference rule, with 𝒞(match, c) ⟿
 -- c-result as the conclusion below the line. 𝒞 carries no state, so its premises
@@ -419,7 +430,7 @@
     rule.name
     rule.label
     Nothing
-    (fst (premisesToLatex rule.premises))
+    (fst (premisesToLatex "e" rule.premises))
     (phinoContextualize (renderExpr rule.match) (renderExpr rule.cmatch) (renderExpr rule.cresult))
 
 -- The state metavariable for index 'n', rendered as s_1, s_2, … to mirror the
@@ -440,27 +451,32 @@
 -- Render a rule's premises in order, threading the state through them. The rule
 -- starts in state s_1; each state-changing premise (𝕄, 𝔻, 𝔼) consumes the
 -- current state and yields the next (s_2, s_3, …), matching how the engine folds
--- the state through the premises ('sidePremise' in 'Dataize.hs'). Returns the
--- rendered judgments and the final state index, which the conclusion returns.
-premisesToLatex :: [Y.Premise] -> ([String], Int)
-premisesToLatex = go 1
+-- the state through the premises ('sidePremise' in 'Dataize.hs'). The 'universe'
+-- is the rule's own e-match, threaded into 𝕄/𝔻 premises (bound by the conclusion)
+-- rather than a free 'e'. Returns the rendered judgments and the final state
+-- index, which the conclusion returns.
+premisesToLatex :: String -> [Y.Premise] -> ([String], Int)
+premisesToLatex universe = go 1
   where
+    go :: Int -> [Y.Premise] -> ([String], Int)
     go index [] = ([], index)
     go index (premise : rest) = (rendered : more, final)
       where
-        (rendered, next) = premiseToLatex index premise
+        (rendered, next) = premiseToLatex universe index premise
         (more, final) = go next rest
 
 -- One premise judgment in state s_index, rendered per its operation. The
--- state-changing operations 𝕄 ('morph'), 𝔻 ('dataize') and 𝔼 ('evaluate') carry
--- the universe 'e' they were given, consume s_index and yield s_index+1 (so they
--- return the bumped index); the rest are stateless and leave the index as is.
-premiseToLatex :: Int -> Y.Premise -> (String, Int)
-premiseToLatex index premise = case premise.operation of
-  Y.OpMorph arg -> (phinoMorph (renderExpr arg) "e" (stateName index) (stateName (index + 1)) (renderExpr (ExMeta premise.result)), index + 1)
-  Y.OpDataize arg -> (phinoDataize (renderExpr arg) "e" (stateName index) (stateName (index + 1)) (renderBytes (BtMeta premise.result)), index + 1)
+-- state-changing operations 𝕄 ('morph'), 𝔻 ('dataize') and 𝔼 ('evaluate') consume
+-- s_index and yield s_index+1 (so they return the bumped index); the rest are
+-- stateless and leave the index as is. 𝕄 and 𝔻 carry the rule's own 'universe'
+-- (its e-match) so the premise stays bound by the conclusion instead of naming a
+-- free 'e'; 𝔼 carries the explicit universe from its own operation.
+premiseToLatex :: String -> Int -> Y.Premise -> (String, Int)
+premiseToLatex universe index premise = case premise.operation of
+  Y.OpMorph arg -> (phinoMorph (renderExpr arg) universe (stateName index) (stateName (index + 1)) (renderExpr (ExMeta premise.result)), index + 1)
+  Y.OpDataize arg -> (phinoDataize (renderExpr arg) universe (stateName index) (stateName (index + 1)) (renderBytes (BtMeta premise.result)), index + 1)
   Y.OpNormalize arg -> (phinoNormalize (renderExpr arg) (renderExpr (ExMeta premise.result)), index)
-  Y.OpEvaluate arg universe -> (phinoEvaluate (renderExpr arg) (renderExpr universe) (stateName index) (stateName (index + 1)) (renderExpr (ExMeta premise.result)), index + 1)
+  Y.OpEvaluate arg evalUniverse -> (phinoEvaluate (renderExpr arg) (renderExpr evalUniverse) (stateName index) (stateName (index + 1)) (renderExpr (ExMeta premise.result)), index + 1)
   Y.OpContextualize arg context -> (phinoContextualize (renderExpr arg) (renderExpr context) (renderExpr (ExMeta premise.result)), index)
 
 -- Assemble an inference block from a name, optional label, optional side
diff --git a/src/Render.hs b/src/Render.hs
--- a/src/Render.hs
+++ b/src/Render.hs
@@ -207,6 +207,7 @@
   render EX_META{..} = render meta
   render EX_PHI_MEET{..} = "\\phinoMeet{" <> maybe "" (\p -> T.pack p <> ":") prefix <> render idx <> "}{ " <> render expr <> " }"
   render EX_PHI_AGAIN{..} = "\\phinoAgain{" <> maybe "" (\p -> T.pack p <> ":") prefix <> render idx <> "}"
+  render EX_BYTES{..} = render bytes
 
 instance Render [ATTRIBUTE] where
   render attrs = T.intercalate ", " (map render attrs)
diff --git a/test/CLISpec.hs b/test/CLISpec.hs
--- a/test/CLISpec.hs
+++ b/test/CLISpec.hs
@@ -842,7 +842,7 @@
       withStdin "[[ x -> [[ y -> [[ L> Func ]].q, z -> Q.x(a -> [[ w -> [[ L> Atom ]], L> Hello ]]) ]], L> Package ]]" $
         testCLISucceeded
           ["rewrite", "--canonize", "--sweet", "--flat"]
-          ["⟦ x ↦ ⟦ y ↦ ⟦ λ ⤍ F1 ⟧.q, z ↦ Φ.x( a ↦ ⟦ w ↦ ⟦ λ ⤍ F2 ⟧, λ ⤍ F3 ⟧ ) ⟧, λ ⤍ F4 ⟧"]
+          ["⟦ x ↦ ⟦ y ↦ ⟦ λ ⤍ Fn1 ⟧.q, z ↦ Φ.x( a ↦ ⟦ w ↦ ⟦ λ ⤍ Fn2 ⟧, λ ⤍ Fn3 ⟧ ) ⟧, λ ⤍ Fn4 ⟧"]
 
     it "rewrites by locator" $
       withStdin "[[ ex -> [[ x -> [[ y -> 5 ]].y ]], abc -> [[ x -> ? ]](x -> 5) ]]" $
@@ -882,12 +882,31 @@
               , "  \\leadsto [[ |x| -> [[ D> |01-|, |y| -> ? ]] ( |y| -> [[]] ) ]] . |x| \\leadsto_{\\nameref{r:copy}}"
               , "  \\leadsto [[ |x| -> [[ D> |01-|, |y| -> [[]] ]] ]] . |x| \\leadsto_{\\nameref{r:dot}}"
               , "  \\leadsto [[ D> |01-|, |y| -> [[]] ]] ( \\phiTerminal{\\rho} -> [[ |x| -> [[ D> |01-|, |y| -> [[]] ]] ]] ) \\leadsto_{\\nameref{r:copy}}"
-              , "  \\leadsto [[ D> |01-|, |y| -> [[]], \\phiTerminal{\\rho} -> [[ |x| -> [[ D> |01-|, |y| -> [[]] ]] ]] ]]{.}"
+              , "  \\leadsto [[ D> |01-|, |y| -> [[]], \\phiTerminal{\\rho} -> [[ |x| -> [[ D> |01-|, |y| -> [[]] ]] ]] ]] \\leadsto_{\\nameref{r:delta}}"
+              , "  \\leadsto |01-|{.}"
               , "\\end{phiquation}"
               , "01-"
               ]
           ]
 
+    it "keeps the delta step in --sequence under --quiet" $
+      withStdin "[[ D> 01- ]]" $
+        testCLISucceeded
+          ["dataize", "--sequence", "--quiet", "--output=latex", "--flat", "--sweet"]
+          [ intercalate
+              "\n"
+              [ "[[ D> |01-| ]] \\leadsto_{\\nameref{r:delta}}"
+              , "  \\leadsto |01-|{.}"
+              , "\\end{phiquation}"
+              ]
+          ]
+
+    it "ends the phi --sequence at the bare data" $
+      withStdin "[[ D> 01- ]]" $
+        testCLISucceeded
+          ["dataize", "--sequence", "--quiet", "--flat", "--sweet"]
+          ["⟦ Δ ⤍ 01- ⟧\n01-"]
+
     it "focuses a compressed sequence whose meet replaces a step root" $
       withStdin "[[ @ -> [[ @ -> $.c.plus( 32.0 ), c -> 25.0 ]], bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus -> [[ x -> ?, L> L_number_plus ]] ]] ]]" $
         testCLISucceeded
@@ -1063,14 +1082,14 @@
             , "\\begin{phinoMorphingInference}"
             , "  \\phinoName{ml}"
             , "  \\phinoLabel{\\lambda}"
-            , "  \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ e_1 }{ s_2 } }"
-            , "  \\phinoPremise{ \\phinoNormalize{ e_1 . \\tau }{ n_1 } }"
-            , "  \\phinoPremise{ \\phinoMorph{ n_1 }{ e }{ s_2 }{ n_2 }{ s_3 } }"
-            , "  \\phinoConclusion{ \\phinoMorph{ [[ B_1, L> F, B_2 ]] . \\tau }{ e }{ s_1 }{ n_2 }{ s_3 } }"
+            , "  \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ n_1 }{ s_2 } }"
+            , "  \\phinoPremise{ \\phinoNormalize{ n_1 . \\tau }{ n_2 } }"
+            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ s_2 }{ n_3 }{ s_3 } }"
+            , "  \\phinoConclusion{ \\phinoMorph{ [[ B_1, L> F, B_2 ]] . \\tau }{ e }{ s_1 }{ n_3 }{ s_3 } }"
             , "\\end{phinoMorphingInference}"
             , "\\begin{phinoMorphingInference}"
             , "  \\phinoName{mphi}"
-            , "  \\phinoLabel{\\phi}"
+            , "  \\phinoLabel{\\varphi}"
             , "  \\phinoCondition{ @ \\in B \\;\\text{and}\\; \\tau \\notin B \\;\\text{and}\\; L \\notin B }"
             , "  \\phinoPremise{ \\phinoNormalize{ [[ B ]] . @ . \\tau }{ n } }"
             , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ n_1 }{ s_2 } }"
@@ -1129,7 +1148,7 @@
             , "\\end{phinoMorphingInference}"
             , "\\begin{phinoMorphingInference}"
             , "  \\phinoName{mg}"
-            , "  \\phinoPremise{ \\phinoMorph{ T }{ e }{ s_1 }{ n }{ s_2 } }"
+            , "  \\phinoPremise{ \\phinoMorph{ T }{ Q }{ s_1 }{ n }{ s_2 } }"
             , "  \\phinoConclusion{ \\phinoMorph{ Q }{ Q }{ s_1 }{ n }{ s_2 } }"
             , "\\end{phinoMorphingInference}"
             ]
@@ -1154,8 +1173,7 @@
             , "\\end{phinoDataizationInference}"
             , "\\begin{phinoDataizationInference}"
             , "  \\phinoName{fire}"
-            , "  \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ e_1 }{ s_2 } }"
-            , "  \\phinoPremise{ \\phinoNormalize{ e_1 }{ n_1 } }"
+            , "  \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ n_1 }{ s_2 } }"
             , "  \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ s_2 }{ \\delta }{ s_3 } }"
             , "  \\phinoConclusion{ \\phinoDataize{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ \\delta }{ s_3 } }"
             , "\\end{phinoDataizationInference}"
diff --git a/test/DataizeSpec.hs b/test/DataizeSpec.hs
--- a/test/DataizeSpec.hs
+++ b/test/DataizeSpec.hs
@@ -281,10 +281,11 @@
                    , "contextualize"
                    , "dot"
                    , "copy"
+                   , "delta"
                    ]
     it "dataizes a located reference through the expected rules" $ do
       labels <- labelsOf "Q.foo.bar" "[[ foo -> [[ bar -> [[ @ -> Q.x ]] ]], x -> [[ D> 42- ]] ]]"
-      labels `shouldBe` ["contextualize", "md", "dot", "copy", "mf"]
+      labels `shouldBe` ["contextualize", "md", "dot", "copy", "mf", "delta"]
     -- The 'none' rule dataizes ⊥ (𝔻(⟦⟧) → 𝔻(⊥)), which matches no clause now
     -- that there is no 'end' rule, so an empty formation reduces through one
     -- labelled 'dataize' step and then fails: it has nothing to dataize (#955).
diff --git a/test/LaTeXSpec.hs b/test/LaTeXSpec.hs
--- a/test/LaTeXSpec.hs
+++ b/test/LaTeXSpec.hs
@@ -10,10 +10,12 @@
 
 import AST (Expression (ExMeta))
 import Control.Monad (forM_)
+import Data.List (intercalate)
 import Data.Text qualified as T
-import LaTeX (LatexContext (..), conditionToLatex, defaultLatexContext, meetInExpression, meetInExpressions)
+import LaTeX (LatexContext (..), conditionToLatex, defaultLatexContext, meetInExpression, meetInExpressions, rewrittensToLatex)
+import Lining (LineFormat (MULTILINE))
 import Parser (parseExpressionThrows)
-import Test.Hspec (Spec, describe, expectationFailure, it, shouldBe)
+import Test.Hspec (Spec, describe, expectationFailure, it, shouldBe, shouldContain)
 import Yaml qualified as Y
 
 spec :: Spec
@@ -48,6 +50,21 @@
       case meetInExpressions exprs ctx of
         (firstStep : _) -> T.count "ExPhiMeet" (T.pack (show firstStep)) `shouldBe` 2
         [] -> expectationFailure "meetInExpressions returned no expressions"
+
+  describe "indents wrapped continuation steps in a --sequence (#981)" $
+    it "nests a wrapped step's members below its two-space \\leadsto line and aligns the closing bracket with it, rather than laying the step out from column 0" $ do
+      start <- parseExpressionThrows "[[ x -> Q.y ]]"
+      wrapped <- parseExpressionThrows "[[ a -> Q.b, c -> Q.d ]]"
+      let ctx = defaultLatexContext{_line = MULTILINE, _margin = 20}
+      latex <- rewrittensToLatex ([(start, Just "first"), (wrapped, Just "second")], False) ctx
+      latex
+        `shouldContain` intercalate
+          "\n"
+          [ "  \\leadsto [["
+          , "    |a| -> Q . |b|,"
+          , "    |c| -> Q . |d|"
+          , "  ]] \\leadsto_{\\nameref{r:second}}"
+          ]
 
   describe "renders the 'formation' condition" $
     forM_
diff --git a/test/YamlSpec.hs b/test/YamlSpec.hs
--- a/test/YamlSpec.hs
+++ b/test/YamlSpec.hs
@@ -75,23 +75,22 @@
       (labels \\ nub labels) `shouldBe` []
 
   describe "reserves 𝑛-family metas for normal forms" $
-    -- 𝒞 ('contextualize') and 𝔼 ('evaluate') return an expression that is not
-    -- necessarily a normal form — that is why a 'normalize' premise follows
-    -- them — so binding their result to an 𝑛-reserved meta (internal prefix
-    -- "n") in a morphing or dataization rule conflates the calculus's 'e'
-    -- (expression) with 'n' (normal form). Such a slip is notational, not
-    -- functional (the meta name is only a substitution-map key), so it is easy
-    -- to miss by eye; flag it automatically instead. Contextualization is
-    -- excluded on purpose: its 𝒞-valued results are the point and its header
-    -- reserves nothing (see #971).
-    it "no contextualize/evaluate premise in a morphing or dataization rule binds an 𝑛-reserved meta" $ do
+    -- 𝒞 ('contextualize') returns an expression that is not necessarily a normal
+    -- form — that is why a 'normalize' premise follows it — so binding its result
+    -- to an 𝑛-reserved meta (internal prefix "n") in a morphing or dataization
+    -- rule conflates the calculus's 'e' (expression) with 'n' (normal form). Such
+    -- a slip is notational, not functional (the meta name is only a
+    -- substitution-map key), so it is easy to miss by eye; flag it automatically
+    -- instead. 𝔼 ('evaluate') is excluded on purpose (partially reverting #971):
+    -- it normalizes its atom's result internally, so its codomain is 𝓝 and an
+    -- 𝑛-family result is exactly right (see #990). Contextualization keeps being
+    -- flagged: its 𝒞-valued results are non-normal (see #971).
+    it "no contextualize premise in a morphing or dataization rule binds an 𝑛-reserved meta" $ do
       let expressionValued :: Operation -> Bool
           expressionValued OpContextualize{} = True
-          expressionValued OpEvaluate{} = True
           expressionValued _ = False
           verbOf :: Operation -> String
           verbOf OpContextualize{} = "contextualize"
-          verbOf OpEvaluate{} = "evaluate"
           verbOf _ = "?"
           premisesOf :: [(String, [Premise])]
           premisesOf =