diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -19,11 +19,11 @@
 This is a command-line normalizer, rewriter, and dataizer
 of [𝜑-calculus](https://www.eolang.org) expressions.
 
-First, you write a simple [𝜑-calculus](https://www.eolang.org) program
+First, you write a simple [𝜑-calculus](https://www.eolang.org) expression
 in the `hello.phi` file:
 
 ```text
-Φ ↦ ⟦ φ ↦ ⟦ Δ ⤍ 68-65-6C-6C-6F ⟧, t ↦ ξ.k, k ↦ ⟦⟧ ⟧
+⟦ φ ↦ ⟦ Δ ⤍ 68-65-6C-6C-6F ⟧, t ↦ ξ.k, k ↦ ⟦⟧ ⟧
 ```
 
 ## Installation
@@ -93,7 +93,7 @@
 
 ## Dataize
 
-Then, you dataize the program:
+Then, you dataize the expression:
 
 ```bash
 $ phino dataize hello.phi
@@ -116,7 +116,7 @@
 
 ```bash
 $ phino rewrite --rule=my-rule.yml hello.phi
-Φ ↦ ⟦ φ ↦ ⟦ Δ ⤍ 62-79-65 ⟧, t ↦ ξ.k, k ↦ ⟦⟧ ⟧
+⟦ φ ↦ ⟦ Δ ⤍ 62-79-65 ⟧, t ↦ ξ.k, k ↦ ⟦⟧ ⟧
 ```
 
 If you want to use many rules, just use `--rule` as many times as you need:
@@ -135,8 +135,8 @@
 If no input file is provided, the 𝜑-expression is taken from `stdin`:
 
 ```bash
-$ echo 'Φ ↦ ⟦ φ ↦ ⟦ Δ ⤍ 68-65-6C-6C-6F ⟧ ⟧' | phino rewrite --rule=my-rule.yml
-Φ ↦ ⟦ φ ↦ ⟦ Δ ⤍ 62-79-65 ⟧ ⟧
+$ echo '⟦ φ ↦ ⟦ Δ ⤍ 68-65-6C-6C-6F ⟧ ⟧' | phino rewrite --rule=my-rule.yml
+⟦ φ ↦ ⟦ Δ ⤍ 62-79-65 ⟧ ⟧
 ```
 
 You're able to pass [`XMIR`][xmir] as input. Use `--input=xmir` and `phino`
@@ -152,8 +152,8 @@
 and print it in canonical syntax:
 
 ```bash
-$ echo 'Q -> [[ @ -> Q.io.stdout("hello") ]]' | phino rewrite
-Φ ↦ ⟦
+$ echo '[[ @ -> Q.io.stdout("hello") ]]' | phino rewrite
+⟦
   φ ↦ Φ.io.stdout(
     α0 ↦ Φ.string(
       α0 ↦ Φ.bytes(
@@ -166,35 +166,35 @@
 
 ## Merge
 
-You can merge several 𝜑-programs into a single one by merging their
+You can merge several 𝜑-expressions into a single one by merging their
 top level formations:
 
 ```bash
 $ cat bytes.phi
-{⟦ bytes(data) ↦ ⟦ φ ↦ data ⟧ ⟧}
+⟦ bytes(data) ↦ ⟦ φ ↦ data ⟧ ⟧
 $ cat number.phi
-{⟦
+⟦
   number(as-bytes) ↦ ⟦
     φ ↦ as-bytes,
     plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧
   ⟧
-⟧}
+⟧
 $ cat minus.phi
-{⟦ number ↦ ⟦ minus(x) ↦ ⟦ λ ⤍ L_number_minus ⟧ ⟧ ⟧}
+⟦ number ↦ ⟦ minus(x) ↦ ⟦ λ ⤍ L_number_minus ⟧ ⟧ ⟧
 $ phino merge bytes.phi number.phi minus.phi --sweet
-{⟦
+⟦
   bytes(data) ↦ ⟦ φ ↦ data ⟧,
   number(as-bytes) ↦ ⟦
     φ ↦ as-bytes,
     plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧,
     minus(x) ↦ ⟦ λ ⤍ L_number_minus ⟧
   ⟧
-⟧}
+⟧
 ```
 
 ## Match
 
-You can test the 𝜑-program matches against the [rule](#rule-structure)
+You can test the 𝜑-expression matches against the [rule](#rule-structure)
 pattern. The result output contains matched substitutions:
 
 ```bash
@@ -287,7 +287,7 @@
 ## Rule structure
 
 This is BNF-like yaml rule structure. Here types ended with
-apostrophe, like `Attribute'` are built types from 𝜑-program [AST](src/AST.hs)
+apostrophe, like `Attribute'` are built types from 𝜑-expression [AST](src/AST.hs)
 
 ```bnfc
 Rule:
diff --git a/benchmark/Main.hs b/benchmark/Main.hs
--- a/benchmark/Main.hs
+++ b/benchmark/Main.hs
@@ -13,8 +13,8 @@
 import Lining (LineFormat (MULTILINE, SINGLELINE))
 import Margin (defaultMargin)
 import Must (Must (MtDisabled))
-import Parser (parseProgramThrows)
-import Printer (printProgram')
+import Parser (parseExpressionThrows)
+import Printer (printExpression')
 import Rewriter (RewriteContext (RewriteContext), rewrite)
 import Sugar (SugarType (SALTY, SWEET))
 import Text.Printf (printf)
@@ -87,16 +87,16 @@
 main = do
   src <- readFile "benchmark/tmp/native.phi"
   xsrc <- readFile "benchmark/tmp/Native.xmir"
-  prog <- parseProgramThrows src
-  runBench "parse/phi" (parseProgramThrows src)
+  expr <- parseExpressionThrows src
+  runBench "parse/phi" (parseExpressionThrows src)
   runBench "parse/xmir" (parseXMIRThrows xsrc >>= xmirToPhi)
-  runBench "rewrite/normalize" (rewrite prog normalizationRules rewriteCtx)
+  runBench "rewrite/normalize" (rewrite expr normalizationRules rewriteCtx)
   runBench
     "print/sweet/multiline"
-    (evaluate (length (printProgram' prog (SWEET, UNICODE, MULTILINE, defaultMargin))))
+    (evaluate (length (printExpression' expr (SWEET, UNICODE, MULTILINE, defaultMargin))))
   runBench
     "print/sweet/flat"
-    (evaluate (length (printProgram' prog (SWEET, UNICODE, SINGLELINE, defaultMargin))))
+    (evaluate (length (printExpression' expr (SWEET, UNICODE, SINGLELINE, defaultMargin))))
   runBench
     "print/salty/multiline"
-    (evaluate (length (printProgram' prog (SALTY, UNICODE, MULTILINE, defaultMargin))))
+    (evaluate (length (printExpression' expr (SALTY, UNICODE, MULTILINE, defaultMargin))))
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.99
+version: 0.0.100
 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/morphing.yaml b/resources/morphing.yaml
--- a/resources/morphing.yaml
+++ b/resources/morphing.yaml
@@ -33,10 +33,12 @@
 # normal-form meta, so the split is total over the normal forms 𝕄 actually
 # sees: 'ma'/'maa' take a '𝑘' argument — absolute (xi-free) and in normal
 # form — and recurse by re-normalizing the application; 'mad'/'maad' take an
-# '𝑛' argument (a normal form) that is 'not (absolute 𝑛1)' and yield ⊥ with
-# no recursion. A non-absolute argument can never fill a slot, so ⊥ is the
-# correct outcome and morphing stays total: exactly one of the four fires,
-# and the ⊥ axioms add no regress. Without them, a void slot receiving a
+# '𝑛' argument (a normal form) that is 'not (absolute 𝑛1)' and yield ⊥
+# through a single 'morph: ⊥' premise, which terminates at once via the
+# 'dead' axiom (𝕄(⊥, e, s) → (⊥, s)) — no recursion. A non-absolute argument
+# can never fill a slot, so ⊥ is the correct outcome and morphing stays
+# total: exactly one of the four fires, and these ⊥ premises add no regress.
+# Without them, a void slot receiving a
 # non-absolute argument — e.g. ⟦ x ↦ ∅ ⟧( x ↦ ξ.foo ) — had no terminating
 # derivation: 'copy' cannot fire on a non-absolute argument, so 'ma'
 # re-morphed the identical stuck term forever.
@@ -103,18 +105,24 @@
 - name: mad
   match: '𝑛(𝜏 ↦ 𝑛1)'
   e-match: 𝑒
-  n-result: ⊥
+  n-result: 𝑛2
   when:
     not:
       absolute: 𝑛1
+  premises:
+    - n-result: 𝑛2
+      morph: ⊥
 
 - name: maad
   match: '𝑛(α𝑖 ↦ 𝑛1)'
   e-match: 𝑒
-  n-result: ⊥
+  n-result: 𝑛2
   when:
     not:
       absolute: 𝑛1
+  premises:
+    - n-result: 𝑛2
+      morph: ⊥
 
 - name: universe
   label: \Phi
diff --git a/src/AST.hs b/src/AST.hs
--- a/src/AST.hs
+++ b/src/AST.hs
@@ -7,7 +7,7 @@
 -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 -- SPDX-License-Identifier: MIT
 
--- This module represents AST tree for parsed phi-calculus program
+-- This module represents AST tree for parsed phi-calculus expression
 module AST where
 
 import Data.Bits (xor)
@@ -16,9 +16,6 @@
 import qualified Data.Text as T
 import GHC.Generics (Generic)
 
-newtype Program = Program Expression
-  deriving (Eq, Ord, Show)
-
 data Expression
   = ExFormation [Binding]
   | ExXi
@@ -171,11 +168,25 @@
     BaseObject label = ExDispatch ExRoot (AtLabel label)
 
 -- Minimal matcher function (required for view pattern)
+--
+-- The primitive→bytes binding is named 'as-bytes' and the bytes→payload
+-- binding is named 'data' (jeo-maven-plugin 0.15.3+, following phi-calculus
+-- dropping positional attributes). The legacy positional α0 form is still
+-- recognized so XMIR produced by older jeo versions keeps sugaring back.
 matchDataObject :: Expression -> Maybe (T.Text, Bytes)
-matchDataObject (ExApplication outer (ArAlpha (Alpha 0) inner)) = case (matchOuter outer, matchInner inner) of
-  (Just label, Just bts) -> Just (label, bts)
-  _ -> Nothing
+matchDataObject (ExApplication outer arg)
+  | Just inner <- asBytesArg arg = case (matchOuter outer, matchInner inner) of
+      (Just label, Just bts) -> Just (label, bts)
+      _ -> Nothing
   where
+    asBytesArg :: Argument -> Maybe Expression
+    asBytesArg (ArTau (AtLabel "as-bytes") inner) = Just inner
+    asBytesArg (ArAlpha (Alpha 0) inner) = Just inner
+    asBytesArg _ = Nothing
+    dataArg :: Argument -> Maybe Expression
+    dataArg (ArTau (AtLabel "data") formation) = Just formation
+    dataArg (ArAlpha (Alpha 0) formation) = Just formation
+    dataArg _ = Nothing
     matchOuter :: Expression -> Maybe T.Text
     matchOuter (BaseObject label) = Just label
     matchOuter (ExPhiAgain _ _ (BaseObject label)) = Just label
@@ -184,9 +195,10 @@
     matchInner (ExPhiAgain _ _ inner') = matchInner inner'
     matchInner inner' = matchInner' inner'
     matchInner' :: Expression -> Maybe Bytes
-    matchInner' (ExApplication bytes (ArAlpha (Alpha 0) formation)) = case (matchesBytes bytes, matchFormation formation) of
-      (True, Just bts) -> Just bts
-      _ -> Nothing
+    matchInner' (ExApplication bytes arg')
+      | Just formation <- dataArg arg' = case (matchesBytes bytes, matchFormation formation) of
+          (True, Just bts) -> Just bts
+          _ -> Nothing
     matchInner' _ = Nothing
     matchesBytes :: Expression -> Bool
     matchesBytes (BaseObject "bytes") = True
@@ -210,12 +222,12 @@
     DataObject label bts =
       ExApplication
         (BaseObject label)
-        ( ArAlpha
-            (Alpha 0)
+        ( ArTau
+            (AtLabel "as-bytes")
             ( ExApplication
                 (BaseObject "bytes")
-                ( ArAlpha
-                    (Alpha 0)
+                ( ArTau
+                    (AtLabel "data")
                     (ExFormation [BiDelta bts, BiVoid AtRho])
                 )
             )
diff --git a/src/CLI/Helpers.hs b/src/CLI/Helpers.hs
--- a/src/CLI/Helpers.hs
+++ b/src/CLI/Helpers.hs
@@ -18,16 +18,16 @@
 import Encoding
 import Files (ensuredFile)
 import Functions (execFunctions)
-import LaTeX (LatexContext (..), defaultMeetLength, defaultMeetPopularity, expressionToLaTeX, programToLaTeX, rewrittensToLatex)
+import LaTeX (LatexContext (..), defaultMeetLength, defaultMeetPopularity, expressionToLaTeX, rewrittensToLatex)
 import Locator (locatedExpression)
 import Logger
-import Parser (parseProgramThrows)
+import Parser (parseExpressionThrows)
 import qualified Printer as P
 import qualified Random as R
 import Rewriter (Rewrittens')
 import System.IO (getContents')
 import Text.Printf (printf)
-import XMIR (parseXMIRThrows, printXMIR, programToXMIR, xmirToPhi)
+import XMIR (expressionToXMIR, parseXMIRThrows, printXMIR, xmirToPhi)
 import Yaml (normalizationRules)
 import qualified Yaml as Y
 
@@ -38,8 +38,8 @@
 justMeetLength = fromMaybe defaultMeetLength
 
 -- Prepare saveStepFunc
-saveStepFunc :: Maybe FilePath -> PrintProgramContext -> SaveStepFunc
-saveStepFunc stepsDir ctx@PrintProgCtx{..} = saveStep stepsDir ioToExt (printProgram ctx)
+saveStepFunc :: Maybe FilePath -> PrintContext -> SaveStepFunc
+saveStepFunc stepsDir ctx@PrintCtx{..} = saveStep stepsDir ioToExt (printInFormat ctx)
   where
     ioToExt :: String
     ioToExt
@@ -56,34 +56,33 @@
     logDebug "Reading from stdin"
     getContents' `catch` (\(e :: SomeException) -> throwIO (CouldNotReadFromStdin (show e)))
 
--- Parse program from String input depending on input IO format
-parseProgram :: String -> IOFormat -> IO Program
-parseProgram phi PHI = parseProgramThrows phi
-parseProgram xmir XMIR = parseXMIRThrows xmir >>= xmirToPhi
-parseProgram _ LATEX = invalidCLIArguments "LaTeX cannot be used as input format"
+-- Parse expression from String input depending on input IO format
+parseInput :: String -> IOFormat -> IO Expression
+parseInput phi PHI = parseExpressionThrows phi
+parseInput xmir XMIR = parseXMIRThrows xmir >>= xmirToPhi
+parseInput _ LATEX = invalidCLIArguments "LaTeX cannot be used as input format"
 
-printRewrittens :: PrintProgramContext -> Rewrittens' -> IO String
-printRewrittens ctx@PrintProgCtx{..} rewrittens@(chain, _)
+printRewrittens :: PrintContext -> Rewrittens' -> IO String
+printRewrittens ctx@PrintCtx{..} rewrittens@(chain, _)
   | _outputFormat == LATEX && _sequence = rewrittensToLatex rewrittens (printCtxToLatexCtx ctx)
-  | _focus == ExRoot = mapM (printProgram ctx . fst) chain <&> intercalate "\n"
-  | otherwise = mapM (\(prog, _) -> locatedExpression _focus prog >>= printExpression ctx) chain <&> intercalate "\n"
+  | _focus == ExRoot = mapM (printInFormat ctx . fst) chain <&> intercalate "\n"
+  | otherwise = mapM (\(expr, _) -> locatedExpression _focus expr >>= printExpression ctx) chain <&> intercalate "\n"
 
-printExpression :: PrintProgramContext -> Expression -> IO String
-printExpression ctx@PrintProgCtx{..} ex = case _outputFormat of
+printExpression :: PrintContext -> Expression -> IO String
+printExpression ctx@PrintCtx{..} ex = case _outputFormat of
   PHI -> pure (P.printExpression' ex (_sugar, UNICODE, _line, _margin))
   XMIR -> throwIO CouldNotPrintExpressionInXMIR
   LATEX -> pure (expressionToLaTeX ex (printCtxToLatexCtx ctx))
 
--- Convert
--- Convert program to corresponding String format
-printProgram :: PrintProgramContext -> Program -> IO String
-printProgram ctx@PrintProgCtx{..} prog = case _outputFormat of
-  PHI -> pure (P.printProgram' prog (_sugar, UNICODE, _line, _margin))
-  XMIR -> programToXMIR prog _xmirCtx <&> printXMIR
-  LATEX -> pure (programToLaTeX prog (printCtxToLatexCtx ctx))
+-- Convert an expression to its corresponding String format
+printInFormat :: PrintContext -> Expression -> IO String
+printInFormat ctx@PrintCtx{..} expr = case _outputFormat of
+  PHI -> pure (P.printExpression' expr (_sugar, UNICODE, _line, _margin))
+  XMIR -> expressionToXMIR expr _xmirCtx <&> printXMIR
+  LATEX -> pure (expressionToLaTeX expr (printCtxToLatexCtx ctx))
 
-printCtxToLatexCtx :: PrintProgramContext -> LatexContext
-printCtxToLatexCtx PrintProgCtx{..} =
+printCtxToLatexCtx :: PrintContext -> LatexContext
+printCtxToLatexCtx PrintCtx{..} =
   LatexContext _sugar _line _margin _nonumber _compress _meetPopularity _meetLength _focus _expression _label _meetPrefix
 
 -- Get rules for rewriting depending on provided flags
diff --git a/src/CLI/Parsers.hs b/src/CLI/Parsers.hs
--- a/src/CLI/Parsers.hs
+++ b/src/CLI/Parsers.hs
@@ -51,7 +51,7 @@
 optRule = many (strOption (long "rule" <> metavar "[FILE]" <> help "Path to custom rule"))
 
 optInputFormat :: Parser IOFormat
-optInputFormat = option (parseIOFormat "input") (long "input" <> metavar "FORMAT" <> help "Program input format (phi, xmir)" <> value PHI <> showDefault)
+optInputFormat = option (parseIOFormat "input") (long "input" <> metavar "FORMAT" <> help "Expression input format (phi, xmir)" <> value PHI <> showDefault)
 
 parseIOFormat :: String -> ReadM IOFormat
 parseIOFormat type' = eitherReader $ \format -> case (map toLower format, type') of
@@ -64,7 +64,7 @@
 optOutputFormat =
   option
     (parseIOFormat "output")
-    (long "output" <> metavar "FORMAT" <> help (printf "Result and intermediate (see %s option(s)) programs output format (phi, xmir, latex)" _intermediateOptions) <> value PHI <> showDefault)
+    (long "output" <> metavar "FORMAT" <> help (printf "Result and intermediate (see %s option(s)) expressions output format (phi, xmir, latex)" _intermediateOptions) <> value PHI <> showDefault)
 
 argInputFile :: Parser (Maybe FilePath)
 argInputFile = optional (argument str (metavar "FILE" <> help "Path to input file"))
@@ -85,7 +85,7 @@
 optMargin =
   option
     (auto >>= validateIntOption (> 0) "--margin must be positive")
-    (long "margin" <> help "The maximum right margin for the printed 𝜑-programs or 𝜑-expressions" <> value defaultMargin <> showDefault)
+    (long "margin" <> help "The maximum right margin for the printed 𝜑-expressions" <> value defaultMargin <> showDefault)
 
 optMeetPopularity :: Parser (Maybe Int)
 optMeetPopularity =
@@ -119,7 +119,7 @@
 optNonumber = switch (long "nonumber" <> help "Turn off equation auto numbering in LaTeX rendering (see --output option)")
 
 optSequence :: Parser Bool
-optSequence = switch (long "sequence" <> help "Result output contains all intermediate 𝜑-programs concatenated with EOL")
+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.")
@@ -134,7 +134,7 @@
 optMeetPrefix = optional (strOption (long "meet-prefix" <> metavar "PREFIX" <> help "Prefix to be inserted before index in \\phinoMeet{} and \\phinoAgain{} LaTeX functions, e.g. \\phinoMeet{foo:1}"))
 
 optBreakpoint :: Parser (Maybe FilePath)
-optBreakpoint = optional (strOption (long "breakpoint" <> metavar "FILE" <> help "The name of the first unmatched rule which leads to stopping entire rewriting process and returning original program"))
+optBreakpoint = optional (strOption (long "breakpoint" <> metavar "FILE" <> help "The name of the first unmatched rule which leads to stopping entire rewriting process and returning original expression"))
 
 optHide :: Parser [String]
 optHide =
@@ -142,7 +142,7 @@
     ( strOption
         ( long "hide"
             <> metavar "FQN"
-            <> help "Location of object to exclude from result and intermediate programs after rewriting. Must be a valid dispatch expression; e.g. Q.org.eolang"
+            <> help "Location of object to exclude from result and intermediate expressions after rewriting. Must be a valid dispatch expression; e.g. Q.org.eolang"
         )
     )
 
@@ -153,7 +153,7 @@
         ( long "show"
             <> metavar "FQN"
             <> help
-              "Location of object to include to result and intermediate programs after rewriting. \
+              "Location of object to include to result and intermediate expressions after rewriting. \
               \Must be a valid dispatch expression; e.g. Q.org.eolang. Unlike --hide, can be used only once"
         )
     )
@@ -166,7 +166,7 @@
   strOption
     ( long "focus"
         <> metavar "FQN"
-        <> help "Location of only object to be printed in entire program. Must be a valid dispatch expression; e.g. Q.foo.bar"
+        <> help "Location of only object to be printed in entire expression. Must be a valid dispatch expression; e.g. Q.foo.bar"
         <> value "Q"
         <> showDefault
     )
@@ -193,16 +193,16 @@
 optShuffle = switch (long "shuffle" <> help "Shuffle rules before applying")
 
 optSugar :: Parser SugarType
-optSugar = flag SALTY SWEET (long "sweet" <> help (printf "Print result and intermediate (see %s option(s)) 𝜑-programs using syntax sugar" _intermediateOptions))
+optSugar = flag SALTY SWEET (long "sweet" <> help (printf "Print result and intermediate (see %s option(s)) 𝜑-expressions using syntax sugar" _intermediateOptions))
 
 optSugar' :: Parser SugarType
-optSugar' = flag SALTY SWEET (long "sweet" <> help "Print result 𝜑-program using syntax sugar")
+optSugar' = flag SALTY SWEET (long "sweet" <> help "Print result 𝜑-expression using syntax sugar")
 
 optLineFormat :: Parser LineFormat
-optLineFormat = flag MULTILINE SINGLELINE (long "flat" <> help (printf "Print result and intermediate (see %s option(s)) 𝜑-programs in one line" _intermediateOptions))
+optLineFormat = flag MULTILINE SINGLELINE (long "flat" <> help (printf "Print result and intermediate (see %s option(s)) 𝜑-expressions in one line" _intermediateOptions))
 
 optLineFormat' :: Parser LineFormat
-optLineFormat' = flag MULTILINE SINGLELINE (long "flat" <> help "Print result 𝜑-program in one line")
+optLineFormat' = flag MULTILINE SINGLELINE (long "flat" <> help "Print result 𝜑-expression in one line")
 
 optMust :: Parser Must
 optMust =
@@ -216,7 +216,7 @@
     )
 
 optOmitListing :: Parser Bool
-optOmitListing = switch (long "omit-listing" <> help "Omit full program listing in XMIR output")
+optOmitListing = switch (long "omit-listing" <> help "Omit full expression listing in XMIR output")
 
 optOmitComments :: Parser Bool
 optOmitComments = switch (long "omit-comments" <> help "Omit comments in XMIR output")
@@ -325,7 +325,7 @@
             <$> optLogLevel
             <*> optLogLines
             <*> optInputFormat
-            <*> option (parseIOFormat "output") (long "output" <> metavar "FORMAT" <> help (printf "Result program output format (phi, xmir, latex)") <> value PHI <> showDefault)
+            <*> option (parseIOFormat "output") (long "output" <> metavar "FORMAT" <> help (printf "Result expression output format (phi, xmir, latex)") <> value PHI <> showDefault)
             <*> optSugar'
             <*> optLineFormat'
             <*> optOmitListing
@@ -351,11 +351,11 @@
 commandParser :: Parser Command
 commandParser =
   hsubparser
-    ( command "rewrite" (info rewriteParser (progDesc "Rewrite the 𝜑-program"))
-        <> command "dataize" (info dataizeParser (progDesc "Dataize the 𝜑-program"))
+    ( command "rewrite" (info rewriteParser (progDesc "Rewrite the 𝜑-expression"))
+        <> command "dataize" (info dataizeParser (progDesc "Dataize the 𝜑-expression"))
         <> command "explain" (info explainParser (progDesc "Explain rules in LaTeX format"))
-        <> command "merge" (info mergeParser (progDesc "Merge 𝜑-programs into single one by merging their top level formations"))
-        <> command "match" (info matchParser (progDesc "Match 𝜑-program against provided pattern and build matched substitutions"))
+        <> command "merge" (info mergeParser (progDesc "Merge 𝜑-expressions into single one by merging their top level formations"))
+        <> command "match" (info matchParser (progDesc "Match 𝜑-expression against provided pattern and build matched substitutions"))
     )
 
 optPin :: Parser (Maybe String)
diff --git a/src/CLI/Runners.hs b/src/CLI/Runners.hs
--- a/src/CLI/Runners.hs
+++ b/src/CLI/Runners.hs
@@ -29,7 +29,7 @@
 import Parser (parseExpressionThrows)
 import qualified Printer as P
 import Rewriter
-import Rule (RuleContext (..), matchProgramWithRule)
+import Rule (RuleContext (..), matchExpressionWithRule)
 import System.Directory (doesFileExist, getModificationTime)
 import System.Exit (exitSuccess)
 import Tau (seedTaus)
@@ -48,23 +48,23 @@
   rules <- getRules _normalize _shuffle _rules
   validateBreakpoint _breakpoint rules
   input <- readInput _inputFile
-  program <- parseProgram input _inputFormat
-  seedTaus program
+  expr <- parseInput input _inputFormat
+  seedTaus expr
   logDebug (printf "Amount of rewriting cycles across all the rules: %d, per rule: %d" _maxCycles _maxDepth)
   let listing = case (rules, _inputFormat, _outputFormat) of
         ([], XMIR, XMIR) -> (\_ -> escapeXML input)
         ([], _, _) -> const input
-        (_, _, _) -> (\prog -> P.printProgram' prog (_sugarType, UNICODE, _flat, _margin))
+        (_, _, _) -> (\rewritten -> P.printExpression' rewritten (_sugarType, UNICODE, _flat, _margin))
       xmirCtx = XmirContext _omitListing _omitComments listing
-      printCtx = printProgCtx xmirCtx foc
+      printCtx = toPrintCtx xmirCtx foc
       canonize = if _canonize then C.canonize else id
       exclude = (`F.exclude` excluded)
       include = (`F.include` included)
-  (rewrittens, exceeded) <- rewrite program rules (context loc printCtx)
+  (rewrittens, exceeded) <- rewrite expr rules (context loc printCtx)
   let rewrittens' = canonize $ exclude $ include (if _sequence then NE.toList rewrittens else [NE.last rewrittens])
-  logDebug (printf "Printing rewritten 𝜑-program as %s" (show _outputFormat))
-  progs <- printRewrittens printCtx (rewrittens', exceeded)
-  output _targetFile progs
+  logDebug (printf "Printing rewritten 𝜑-expression as %s" (show _outputFormat))
+  exprs <- printRewrittens printCtx (rewrittens', exceeded)
+  output _targetFile exprs
   where
     validateOpts :: IO ()
     validateOpts = do
@@ -99,25 +99,25 @@
             (rule `elem` names)
             (invalidCLIArguments (printf "The rule '%s' provided in '--breakpoint' option is absent across given rewriting rules: %s" rule (intercalate ", " names)))
     output :: Maybe FilePath -> String -> IO ()
-    output target prog = case (_inPlace, target, _inputFile) of
+    output target expr = case (_inPlace, target, _inputFile) of
       (True, _, Just file) -> do
         logDebug (printf "The option '--in-place' is specified, writing back to '%s'..." file)
-        writeFile file prog
+        writeFile file expr
         logDebug (printf "The file '%s' was modified in-place" file)
       (True, _, Nothing) ->
         error "The option --in-place requires an input file"
       (False, Just file, _) -> do
         logDebug (printf "The option '--target' is specified, printing to '%s'..." file)
-        writeFile file prog
+        writeFile file expr
         logDebug (printf "The command result was saved in '%s'" file)
       (False, Nothing, _) -> do
         logDebug "The option '--target' is not specified, printing to console..."
-        putStrLn prog
-    context :: Expression -> PrintProgramContext -> RewriteContext
+        putStrLn expr
+    context :: Expression -> PrintContext -> RewriteContext
     context loc ctx = RewriteContext loc _maxDepth _maxCycles _depthSensitive buildTerm _must _breakpoint (saveStepFunc _stepsDir ctx)
-    printProgCtx :: XmirContext -> Expression -> PrintProgramContext
-    printProgCtx xmirCtx focus =
-      PrintProgCtx
+    toPrintCtx :: XmirContext -> Expression -> PrintContext
+    toPrintCtx xmirCtx focus =
+      PrintCtx
         _sugarType
         _flat
         _margin
@@ -141,13 +141,13 @@
   [loc] <- validatedDispatches "locator" [_locator]
   [foc] <- validatedDispatches "focus" [_focus]
   input <- readInput _inputFile
-  prog <- parseProgram input _inputFormat
-  seedTaus prog
-  let printCtx = printProgCtx foc
+  expr <- parseInput input _inputFormat
+  seedTaus expr
+  let printCtx = toPrintCtx foc
       canonize = if _canonize then C.canonize else id
       exclude = (`F.exclude` excluded)
       include = (`F.include` included)
-  (bytes, chain) <- dataize prog (context loc printCtx)
+  (bytes, chain) <- dataize expr (context loc printCtx)
   when _sequence (printRewrittens printCtx (canonize $ exclude $ include chain, False) >>= putStrLn)
   unless _quiet (putStrLn (P.printBytes bytes))
   where
@@ -160,11 +160,11 @@
         [(_meetPopularity, "meet-popularity"), (_meetLength, "meet-length")]
       validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] _focus
       when (length _show > 1) (invalidCLIArguments "The option --show can be used only once")
-    context :: Expression -> PrintProgramContext -> DataizeContext
+    context :: Expression -> PrintContext -> DataizeContext
     context loc ctx = DataizeContext loc _maxDepth _maxCycles _depthSensitive _shuffle buildTerm (saveStepFunc _stepsDir ctx)
-    printProgCtx :: Expression -> PrintProgramContext
-    printProgCtx focus =
-      PrintProgCtx
+    toPrintCtx :: Expression -> PrintContext
+    toPrintCtx focus =
+      PrintCtx
         _sugarType
         _flat
         _margin
@@ -201,21 +201,21 @@
 runMerge OptsMerge{..} = do
   validateOpts
   inputs' <- traverse (readInput . Just) _inputs
-  progs <- traverse (`parseProgram` _inputFormat) inputs'
-  prog <- merge progs
-  let listing = const (P.printProgram' prog (_sugarType, UNICODE, _flat, _margin))
+  exprs <- traverse (`parseInput` _inputFormat) inputs'
+  expr <- merge exprs
+  let listing = const (P.printExpression' expr (_sugarType, UNICODE, _flat, _margin))
       xmirCtx = XmirContext _omitListing _omitComments listing
-      printCtx = printProgCtx xmirCtx
-  prog' <- printProgram printCtx prog
-  printOut _targetFile prog'
+      printCtx = toPrintCtx xmirCtx
+  expr' <- printInFormat printCtx expr
+  printOut _targetFile expr'
   where
     validateOpts :: IO ()
     validateOpts = do
       when (null _inputs) (throwIO (InvalidCLIArguments "At least one input file must be specified for 'merge' command"))
       validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] "Q"
-    printProgCtx :: XmirContext -> PrintProgramContext
-    printProgCtx xmirCtx =
-      PrintProgCtx
+    toPrintCtx :: XmirContext -> PrintContext
+    toPrintCtx xmirCtx =
+      PrintCtx
         _sugarType
         _flat
         _margin
@@ -234,14 +234,14 @@
 runMatch :: OptsMatch -> IO ()
 runMatch OptsMatch{..} = do
   input <- readInput _inputFile
-  prog <- parseProgram input PHI
-  seedTaus prog
+  expr <- parseInput input PHI
+  seedTaus expr
   if isNothing _pattern
     then logDebug "The --pattern is not provided, no substitutions are built"
     else do
       ptn <- parseExpressionThrows (fromJust _pattern)
       condition <- traverse parseConditionThrows _when
-      substs <- matchProgramWithRule prog (rule ptn condition) (RuleContext buildTerm)
+      substs <- matchExpressionWithRule expr (rule ptn condition) (RuleContext buildTerm)
       if null substs
         then throwIO EmptySubstsOnMatch
         else putStrLn (P.printSubsts' substs (_sugarType, UNICODE, _flat, defaultMargin))
diff --git a/src/CLI/Types.hs b/src/CLI/Types.hs
--- a/src/CLI/Types.hs
+++ b/src/CLI/Types.hs
@@ -15,7 +15,7 @@
 import Text.Printf (printf)
 import XMIR (XmirContext)
 
-data PrintProgramContext = PrintProgCtx
+data PrintContext = PrintCtx
   { _sugar :: SugarType
   , _line :: LineFormat
   , _margin :: Int
@@ -44,8 +44,8 @@
 instance Show CmdException where
   show (InvalidCLIArguments msg) = printf "Invalid set of arguments: %s" msg
   show (CouldNotReadFromStdin msg) = printf "Could not read input from stdin\nReason: %s" msg
-  show CouldNotDataize = "Could not dataize given program"
-  show CouldNotPrintExpressionInXMIR = "Could not print expression with --output=xmir, only program printing is allowed"
+  show CouldNotDataize = "Could not dataize given expression"
+  show CouldNotPrintExpressionInXMIR = "Could not print expression with --output=xmir, only expression printing is allowed"
   show EmptySubstsOnMatch = "Provided pattern was not matched, no substitutions are built"
   show (VersionMismatch expected actual) =
     printf "Version mismatch: --pin requires '%s', but this is phino %s" expected actual
diff --git a/src/CST.hs b/src/CST.hs
--- a/src/CST.hs
+++ b/src/CST.hs
@@ -7,7 +7,7 @@
 
 -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 -- SPDX-License-Identifier: MIT
--- This module represents concrete syntax tree for phi-calculus program
+-- This module represents concrete syntax tree for phi-calculus expression
 module CST where
 
 import AST
@@ -117,11 +117,6 @@
   | AL_META {sym :: ALPHA', meta :: META}
   deriving (Eq, Show)
 
-data PROGRAM
-  = PR_SWEET {lcb :: LCB, expr :: EXPRESSION, rcb :: RCB, space :: SPACE}
-  | PR_SALTY {global :: GLOBAL, arrow :: ARROW, expr :: EXPRESSION}
-  deriving (Eq, Show)
-
 data PAIR
   = PA_TAU {attr :: ATTRIBUTE, arrow :: ARROW, expr :: EXPRESSION}
   | PA_ALPHA {alpha :: ALPHA, arrow :: ARROW, expr :: EXPRESSION}
@@ -253,9 +248,6 @@
 data EXTRA = EXTRA {meta :: EXTRA_ARG, func :: String, args :: [EXTRA_ARG]}
   deriving (Eq, Show)
 
-programToCST :: Program -> PROGRAM
-programToCST = toCST'
-
 expressionToCST :: Expression -> EXPRESSION
 expressionToCST = toCST'
 
@@ -312,9 +304,6 @@
 -- All further transformations must consider that
 class ToCST a b where
   toCST :: a -> (Int, EOL) -> b
-
-instance ToCST Program PROGRAM where
-  toCST (Program expr) ctx = PR_SWEET LCB (toCST expr ctx) RCB NO_SPACE
 
 instance ToCST Expression EXPRESSION where
   toCST ExRoot _ = EX_GLOBAL Φ
diff --git a/src/Canonizer.hs b/src/Canonizer.hs
--- a/src/Canonizer.hs
+++ b/src/Canonizer.hs
@@ -46,4 +46,4 @@
 
 canonize :: [Rewritten] -> [Rewritten]
 canonize [] = []
-canonize ((Program expr, maybeRule) : rest) = (Program (fst (canonizeExpression expr 1)), maybeRule) : canonize rest
+canonize ((expr, maybeRule) : rest) = (fst (canonizeExpression expr 1), maybeRule) : canonize rest
diff --git a/src/Dataize.hs b/src/Dataize.hs
--- a/src/Dataize.hs
+++ b/src/Dataize.hs
@@ -47,8 +47,8 @@
 -- here: the universe (the second argument 'e' of 𝕄(n, e, s) and 𝔻(n, e, s)) is a
 -- plain expression threaded as an argument to 'dataize'', 'morph' and on to the
 -- atoms, and the state 's' is threaded the same way (see 'State'). The working
--- program needed for normalization is taken from the head of the step chain, so
--- no 'Program' is threaded around.
+-- expression needed for normalization is taken from the head of the step chain,
+-- so no separate wrapper type is threaded around.
 data DataizeContext = DataizeContext
   { _locator :: Expression
   , _maxDepth :: Int
@@ -147,14 +147,15 @@
     sides :: [Y.Premise] -> Subst -> IO (Subst, State)
     sides premises subst = foldM (sidePremise univ ctx) (subst, state) premises
 
--- Dataize the program located at '_locator'. The program's root is the universe
--- (the 'e' argument) passed to 𝔻 and 𝕄.
-dataize :: Program -> DataizeContext -> IO Dataized
-dataize program@(Program univ) ctx@DataizeContext{..} = do
-  expr <- locatedExpression _locator program
+-- Dataize the expression located at '_locator'. The whole input expression is
+-- itself the universe Q (the 'e' argument) threaded through 𝔻 and 𝕄, so it is
+-- passed both as the located target and as the universe.
+dataize :: Expression -> DataizeContext -> IO Dataized
+dataize universe ctx@DataizeContext{..} = do
+  expr <- locatedExpression _locator universe
   -- Dataization starts from the empty state; the final state is not yet
   -- consumed by any caller, so it is discarded here.
-  ((bytes, seq), _state) <- dataize' (expr, (program, Nothing) :| []) univ emptyState ctx
+  ((bytes, seq), _state) <- dataize' (expr, (universe, Nothing) :| []) universe emptyState ctx
   pure (bytes, reverse seq)
 
 -- The Dataization function 𝔻 retrieves bytes from an expression. It is partial
@@ -314,19 +315,19 @@
 verbArgs (Y.OpDataize expr) = [ArgExpression expr]
 
 leadsTo :: NonEmpty Rewritten -> String -> Expression -> DataizeContext -> IO (NonEmpty Rewritten)
-leadsTo ((prog, _) :| rest) rule expr DataizeContext{..} = do
-  prog' <- withLocatedExpression _locator expr prog
-  pure ((prog', Nothing) :| (prog, Just rule) : rest)
+leadsTo ((current, _) :| rest) rule expr DataizeContext{..} = do
+  updated <- withLocatedExpression _locator expr current
+  pure ((updated, Nothing) :| (current, Just rule) : rest)
 
 -- Reduce 'expr' to its normal form through the normalization rewriter, embedding
--- it at '_locator' into the working program taken from the head of the step
+-- it at '_locator' into the working expression taken from the head of the step
 -- chain so the rewriter sees the surrounding context. Splices the individual
 -- steps (alpha, copy, dot, …) into the chain and returns the normalized
 -- expression together with the extended sequence.
 normalized :: Expression -> NonEmpty Rewritten -> DataizeContext -> IO (Expression, NonEmpty Rewritten)
 normalized expr seq ctx@DataizeContext{..} = do
-  prog' <- withLocatedExpression _locator expr (fst (NE.head seq))
-  (rewrittens, _) <- rewrite prog' normalizationRules (rewriteContext ctx)
+  whole <- withLocatedExpression _locator expr (fst (NE.head seq))
+  (rewrittens, _) <- rewrite whole normalizationRules (rewriteContext ctx)
   let (rw :| rws) = NE.reverse rewrittens
       seq' = rw :| rws <> NE.tail seq
   expr' <- locatedExpression _locator (fst rw)
@@ -340,7 +341,7 @@
 
 -- Synthetic dataize function for internal usage inside atoms. Here we modify the
 -- universe by adding a new binding which refers to the expression we want to
--- dataize, building a local working program to reduce within. As a caller of 𝔻,
+-- dataize, building a local working expression to reduce within. As a caller of 𝔻,
 -- it first reduces the expression to a normal form, since 𝔻 only accepts normal
 -- forms. The universe 'univ' itself is forwarded unchanged, so morphing Φ under
 -- this context still resolves to the true universe rather than to this
@@ -349,8 +350,8 @@
 _dataize expr univ state ctx@DataizeContext{_buildTerm = buildTerm} = case univ of
   ExFormation bds -> do
     (TeAttribute attr) <- buildTerm "random-tau" [] substEmpty
-    let prog = Program (ExFormation (BiTau attr expr : bds))
-    (normal, seq) <- normalized expr ((prog, Nothing) :| []) ctx
+    let synthetic = ExFormation (BiTau attr expr : bds)
+    (normal, seq) <- normalized expr ((synthetic, Nothing) :| []) ctx
     ((bts, _), state') <- dataize' (normal, seq) univ state ctx
     pure (bts, state')
   _ -> throwIO (userError "Can't call _dataize from atoms with non-formation universe")
@@ -425,6 +426,6 @@
 _morph :: Expression -> DataizeContext -> State -> BuildTermMethodS
 _morph univ ctx state [ArgExpression expr] subst = do
   built <- buildExpressionThrows expr subst
-  ((morphed, _), state') <- morph (built, (Program univ, Nothing) :| []) univ state ctx
+  ((morphed, _), state') <- morph (built, (univ, Nothing) :| []) univ state ctx
   pure (TeExpression morphed, state')
 _morph _ _ _ _ _ = throwIO (userError "Function morph() requires exactly 1 expression argument")
diff --git a/src/Deps.hs b/src/Deps.hs
--- a/src/Deps.hs
+++ b/src/Deps.hs
@@ -41,14 +41,14 @@
 
 type BuildTermFunc = String -> BuildTermMethod
 
-type SaveStepFunc = Program -> Int -> IO ()
+type SaveStepFunc = Expression -> Int -> IO ()
 
-saveStep :: Maybe FilePath -> String -> (Program -> IO String) -> SaveStepFunc
+saveStep :: Maybe FilePath -> String -> (Expression -> IO String) -> SaveStepFunc
 saveStep Nothing _ _ _ _ = pure ()
-saveStep (Just dir) ext render prog step = do
+saveStep (Just dir) ext render expr step = do
   createDirectoryIfMissing True dir
   let path = dir </> printf "%05d.%s" step ext
-  content <- render prog
+  content <- render expr
   writeFile path content
   logDebug (printf "Saved step '%d' to '%s'" step path)
 
diff --git a/src/Encoding.hs b/src/Encoding.hs
--- a/src/Encoding.hs
+++ b/src/Encoding.hs
@@ -17,10 +17,6 @@
 class ToASCII a where
   toASCII :: a -> a
 
-instance ToASCII PROGRAM where
-  toASCII PR_SALTY{..} = PR_SALTY Q ARROW' (toASCII expr)
-  toASCII PR_SWEET{..} = PR_SWEET lcb (toASCII expr) rcb space
-
 instance ToASCII EXPRESSION where
   toASCII EX_GLOBAL{} = EX_GLOBAL Q
   toASCII EX_XI{} = EX_XI DOLLAR
diff --git a/src/Filter.hs b/src/Filter.hs
--- a/src/Filter.hs
+++ b/src/Filter.hs
@@ -7,11 +7,11 @@
 import Misc
 import Rewriter
 
-exclude' :: Program -> [Expression] -> Program
-exclude' prog [] = prog
-exclude' prog@(Program ex@(ExFormation _)) (fqn : remaining) = case fqnToAttrs fqn of
-  Just fqn' -> exclude' (Program (excludedFormation ex fqn')) remaining
-  _ -> prog
+exclude' :: Expression -> [Expression] -> Expression
+exclude' expr [] = expr
+exclude' expr@(ExFormation _) (fqn : remaining) = case fqnToAttrs fqn of
+  Just fqn' -> exclude' (excludedFormation expr fqn') remaining
+  _ -> expr
   where
     excludedFormation :: Expression -> [Attribute] -> Expression
     excludedFormation (ExFormation bindings) [at] = ExFormation [bd | bd <- bindings, attributeFromBinding bd /= Just at]
@@ -24,19 +24,19 @@
           | otherwise = bd : excludedBindings bs as
         excludedBindings (bd : bs) as = bd : excludedBindings bs as
     excludedFormation e _ = e
-exclude' prog _ = prog
+exclude' expr _ = expr
 
 exclude :: [Rewritten] -> [Expression] -> [Rewritten]
 exclude [] _ = []
 exclude rs [] = rs
-exclude ((program, maybeRule) : rest) exprs = (exclude' program exprs, maybeRule) : exclude rest exprs
+exclude ((expr, maybeRule) : rest) exprs = (exclude' expr exprs, maybeRule) : exclude rest exprs
 
-include' :: Program -> Expression -> Program
-include' (Program ex@(ExFormation _)) fqn =
-  let def = Program (ExFormation [BiVoid AtRho])
+include' :: Expression -> Expression -> Expression
+include' ex@(ExFormation _) fqn =
+  let def = ExFormation [BiVoid AtRho]
    in case fqnToAttrs fqn of
         Just fqn' -> case includedFormation ex fqn' of
-          Just e -> Program e
+          Just e -> e
           _ -> def
         _ -> def
   where
@@ -52,9 +52,9 @@
           | otherwise = includedBindings bs as
         includedBindings _ _ = Nothing
     includedFormation _ _ = Nothing
-include' _ _ = Program (ExFormation [BiVoid AtRho])
+include' _ _ = ExFormation [BiVoid AtRho]
 
 include :: [Rewritten] -> [Expression] -> [Rewritten]
 include [] _ = []
 include rs [] = rs
-include ((program, maybeRule) : rest) (expr : _) = (include' program expr, maybeRule) : include rest [expr]
+include ((expr, maybeRule) : rest) (fqn : _) = (include' expr fqn, maybeRule) : include rest [fqn]
diff --git a/src/Functions.hs b/src/Functions.hs
--- a/src/Functions.hs
+++ b/src/Functions.hs
@@ -26,7 +26,7 @@
 import qualified Yaml as Y
 
 -- Names of build-term functions that need the full evaluation context
--- (program plus atom evaluation) and are therefore provided only by
+-- (expression plus atom evaluation) and are therefore provided only by
 -- 'Dataize.execBuildTerm', not by 'buildTerm'. They are available while
 -- executing dataization and morphing rules, but not rewriting rules.
 execFunctions :: [String]
diff --git a/src/LaTeX.hs b/src/LaTeX.hs
--- a/src/LaTeX.hs
+++ b/src/LaTeX.hs
@@ -14,14 +14,13 @@
   , explainDataizeRules
   , explainContextualizeRules
   , rewrittensToLatex
-  , programToLaTeX
   , expressionToLaTeX
   , defaultLatexContext
   , defaultMeetLength
   , defaultMeetPopularity
   , LatexContext (..)
-  , meetInPrograms
-  , meetInProgram
+  , meetInExpressions
+  , meetInExpression
   , conditionToLatex
   ) where
 
@@ -37,7 +36,7 @@
 import Matcher
 import Misc
 import Render (Render (render))
-import Replacer (replaceProgram)
+import Replacer (replaceExpression)
 import Rewriter (Rewritten, Rewrittens')
 import Sugar (SugarType (SWEET), ToSalty, withSugarType)
 import Text.Printf (printf)
@@ -67,43 +66,43 @@
 defaultMeetLength :: Int
 defaultMeetLength = 8
 
-meetInProgram :: Program -> Int -> Program -> [Expression]
-meetInProgram (Program expr) len = meetInExpression expr
+meetInExpression :: Expression -> Int -> Expression -> [Expression]
+meetInExpression expr len = meetIn expr
   where
-    meetInExpression :: Expression -> Program -> [Expression]
-    meetInExpression (DataString _) _ = []
-    meetInExpression (DataNumber _) _ = []
-    meetInExpression (ExPhiMeet{}) _ = []
-    meetInExpression (ExPhiAgain{}) _ = []
-    meetInExpression ex prog =
-      let matched = if countNodes ex >= len then map (const ex) (matchProgram ex prog) else []
+    meetIn :: Expression -> Expression -> [Expression]
+    meetIn (DataString _) _ = []
+    meetIn (DataNumber _) _ = []
+    meetIn (ExPhiMeet{}) _ = []
+    meetIn (ExPhiAgain{}) _ = []
+    meetIn ex target =
+      let matched = if countNodes ex >= len then map (const ex) (matchExpression ex target) else []
        in matched ++ case ex of
-            ExDispatch ex' _ -> meetInExpression ex' prog
-            ExApplication ex' arg -> meetInExpression ex' prog ++ meetInExpression (argExpr arg) prog
-            ExFormation bds -> meetInBindings bds prog
+            ExDispatch ex' _ -> meetIn ex' target
+            ExApplication ex' arg -> meetIn ex' target ++ meetIn (argExpr arg) target
+            ExFormation bds -> meetInBindings bds target
             _ -> []
-    meetInBindings :: [Binding] -> Program -> [Expression]
+    meetInBindings :: [Binding] -> Expression -> [Expression]
     meetInBindings [] _ = []
-    meetInBindings (BiTau _ ex : bds) prog = meetInExpression ex prog ++ meetInBindings bds prog
-    meetInBindings (_ : bds) prog = meetInBindings bds prog
+    meetInBindings (BiTau _ ex : bds) target = meetIn ex target ++ meetInBindings bds target
+    meetInBindings (_ : bds) target = meetInBindings bds target
     argExpr :: Argument -> Expression
     argExpr (ArTau _ ex) = ex
     argExpr (ArAlpha _ ex) = ex
 
-{- | Here we're trying to compress sequence of programs with \phinoMeet{} and \phinoAgain LaTeX functions.
-We process the sequence of programs and trying to find all expressions in first program which are present
-in following programs. Then we find ONE expression which is the most frequently encountered.
-If it's encountered in more than specific percentage (_meetPopularity) of following programs - we replace
-it with \phinoAgain{} in following programs and with \phinoMeet{} in first program.
+{- | Here we're trying to compress a sequence of expressions with \phinoMeet{} and \phinoAgain LaTeX functions.
+We process the sequence of expressions and trying to find all sub-expressions in the first expression which are present
+in the following expressions. Then we find ONE expression which is the most frequently encountered.
+If it's encountered in more than specific percentage (_meetPopularity) of the following expressions - we replace
+it with \phinoAgain{} in the following expressions and with \phinoMeet{} in the first expression.
 -}
-meetInPrograms :: [Program] -> LatexContext -> [Program]
-meetInPrograms prog LatexContext{..} = go prog 1
+meetInExpressions :: [Expression] -> LatexContext -> [Expression]
+meetInExpressions exprs LatexContext{..} = go exprs 1
   where
-    go :: [Program] -> Int -> [Program]
+    go :: [Expression] -> Int -> [Expression]
     go [] _ = []
-    go [program] _ = [program]
+    go [single] _ = [single]
     go (first : rest) idx =
-      let met = map (meetInProgram first _meetLength) rest
+      let met = map (meetInExpression first _meetLength) rest
           unique = nub (concat met)
           (frequent, _) =
             foldl
@@ -118,15 +117,15 @@
           next = first : go rest idx
        in case frequent of
             Just expr ->
-              case matchProgram expr first of
+              case matchExpression expr first of
                 (_ : substs) ->
                   let met' = map (filter (== expr)) met
-                      program = replaceProgram (first, [expr], [ExPhiMeet _meetPrefix idx])
-                      program' = replaceProgram (program, map (const expr) substs, map (const (ExPhiAgain _meetPrefix idx)) substs)
-                      rest' = zipWith (\prgm exprs -> replaceProgram (prgm, exprs, map (const (ExPhiAgain _meetPrefix idx)) exprs)) rest met'
+                      withMeet = replaceExpression (first, [expr], [ExPhiMeet _meetPrefix idx])
+                      withAgain = replaceExpression (withMeet, map (const expr) substs, map (const (ExPhiAgain _meetPrefix idx)) substs)
+                      rest' = zipWith (\other exprs' -> replaceExpression (other, exprs', map (const (ExPhiAgain _meetPrefix idx)) exprs')) rest met'
                       found = filter (not . null) met'
                    in if length met' > 1 && toDouble (length found) / toDouble (length met') >= popularity
-                        then program' : go rest' (idx + 1)
+                        then withAgain : go rest' (idx + 1)
                         else next
                 [] -> next
             _ -> next
@@ -166,32 +165,29 @@
 
 compressedRewrittens :: [Rewritten] -> LatexContext -> [Rewritten]
 compressedRewrittens rewrittens ctx@LatexContext{..} =
-  let (progs, rules) = unzip rewrittens
-   in if _compress then zip (meetInPrograms progs ctx) rules else rewrittens
+  let (exprs, rules) = unzip rewrittens
+   in if _compress then zip (meetInExpressions exprs ctx) rules else rewrittens
 
 -- Compress a sequence of focused sub-expressions the way 'compressedRewrittens'
--- compresses whole programs: each expression is wrapped as a program so the
--- meet machinery factors recurring sub-expressions out across the sequence.
--- Focusing happens before this, so the meet never replaces a program root the
--- focus must still descend through.
+-- compresses whole expressions: the meet machinery factors recurring
+-- sub-expressions out across the sequence. Focusing happens before this, so the
+-- meet never replaces a root the focus must still descend through.
 compressedExpressions :: [Expression] -> LatexContext -> [Expression]
 compressedExpressions exprs ctx@LatexContext{..} =
-  if _compress then map unwrap (meetInPrograms (map Program exprs) ctx) else exprs
-  where
-    unwrap (Program expr) = expr
+  if _compress then meetInExpressions exprs ctx else exprs
 
 rewrittensToLatex :: Rewrittens' -> LatexContext -> IO String
 rewrittensToLatex (rewrittens, exceeded) ctx@LatexContext{_focus = ExRoot} =
   pure
     ( concat
         [ preamble ctx
-        , body (compressedRewrittens rewrittens ctx) (\prog -> renderToLatex (programToCST prog) ctx)
+        , body (compressedRewrittens rewrittens ctx) (\expr -> renderToLatex (expressionToCST expr) ctx)
         , ending exceeded ctx
         ]
     )
 rewrittensToLatex (rewrittens, exceeded) ctx@LatexContext{..} = do
-  let (progs, rules) = unzip rewrittens
-  focused <- mapM (locatedExpression _focus) progs
+  let (exprs, rules) = unzip rewrittens
+  focused <- mapM (locatedExpression _focus) exprs
   pure
     ( concat
         [ preamble ctx
@@ -200,14 +196,6 @@
         ]
     )
 
-programToLaTeX :: Program -> LatexContext -> String
-programToLaTeX prog ctx =
-  concat
-    [ preamble ctx
-    , renderToLatex (programToCST prog) ctx
-    , ending False ctx
-    ]
-
 expressionToLaTeX :: Expression -> LatexContext -> String
 expressionToLaTeX ex ctx =
   concat
@@ -221,10 +209,6 @@
 
 class ToLaTeX a where
   toLaTeX :: a -> a
-
-instance ToLaTeX PROGRAM where
-  toLaTeX PR_SWEET{..} = PR_SWEET BIG_LCB (toLaTeX expr) BIG_RCB SPACE
-  toLaTeX PR_SALTY{..} = PR_SALTY global arrow (toLaTeX expr)
 
 instance ToLaTeX EXPRESSION where
   toLaTeX EX_ATTR{..} = EX_ATTR (toLaTeX attr)
diff --git a/src/Lining.hs b/src/Lining.hs
--- a/src/Lining.hs
+++ b/src/Lining.hs
@@ -18,10 +18,6 @@
 class ToSingleLine a where
   toSingleLine :: a -> a
 
-instance ToSingleLine PROGRAM where
-  toSingleLine PR_SALTY{..} = PR_SALTY global arrow (toSingleLine expr)
-  toSingleLine PR_SWEET{..} = PR_SWEET lcb (toSingleLine expr) rcb space
-
 instance ToSingleLine EXPRESSION where
   toSingleLine EX_FORMATION{lsb, binding = bd@BI_EMPTY{}, rsb} = EX_FORMATION lsb NO_EOL NO_TAB bd NO_EOL NO_TAB rsb
   toSingleLine EX_FORMATION{..} = EX_FORMATION lsb NO_EOL TAB' (toSingleLine binding) NO_EOL TAB' rsb
diff --git a/src/Locator.hs b/src/Locator.hs
--- a/src/Locator.hs
+++ b/src/Locator.hs
@@ -25,9 +25,9 @@
       (printExpression fqn)
   show CanNotFindObjectByLocator{..} = printf "Can't find object by locator: '%s'" (printExpression fqn)
 
-locatedExpression :: Expression -> Program -> IO Expression
-locatedExpression ExRoot (Program expr) = pure expr
-locatedExpression locator (Program expr) = case fqnToAttrs locator of
+locatedExpression :: Expression -> Expression -> IO Expression
+locatedExpression ExRoot expr = pure expr
+locatedExpression locator expr = case fqnToAttrs locator of
   Just attrs -> locatedExpression' expr attrs
   _ -> invalidLocator locator
   where
@@ -41,10 +41,10 @@
       _ -> cantFindBy locator
     locatedExpression' _ _ = cantFindBy locator
 
-withLocatedExpression :: Expression -> Expression -> Program -> IO Program
-withLocatedExpression ExRoot tgt _ = pure (Program tgt)
-withLocatedExpression locator target (Program expr) = case fqnToAttrs locator of
-  Just attrs -> Program <$> withLocatedExpression' expr attrs
+withLocatedExpression :: Expression -> Expression -> Expression -> IO Expression
+withLocatedExpression ExRoot tgt _ = pure tgt
+withLocatedExpression locator target expr = case fqnToAttrs locator of
+  Just attrs -> withLocatedExpression' expr attrs
   _ -> invalidLocator locator
   where
     withLocatedExpression' :: Expression -> [Attribute] -> IO Expression
diff --git a/src/Margin.hs b/src/Margin.hs
--- a/src/Margin.hs
+++ b/src/Margin.hs
@@ -21,12 +21,6 @@
 class WithMargin a where
   withMargin' :: (Int, Int) -> a -> a
 
-instance WithMargin PROGRAM where
-  withMargin' (_, margin) PR_SWEET{..} = PR_SWEET lcb (withMargin' (2, margin) expr) rcb space
-  withMargin' (_, margin) PR_SALTY{..} =
-    let before = lengthOf global + lengthOf arrow + 2 -- 'Q -> '
-     in PR_SALTY global arrow (withMargin' (before, margin) expr)
-
 instance WithMargin EXPRESSION where
   withMargin' _ ex@EX_FORMATION{binding = BI_EMPTY{}} = ex
   withMargin' (extra, margin) ex@EX_FORMATION{tab = tab@(TAB indent), ..} =
diff --git a/src/Matcher.hs b/src/Matcher.hs
--- a/src/Matcher.hs
+++ b/src/Matcher.hs
@@ -140,6 +140,3 @@
 
 matchExpression :: MatchExpressionFunc
 matchExpression = matchExpressionDeep
-
-matchProgram :: Expression -> Program -> [Subst]
-matchProgram ptn (Program expr) = matchExpression ptn expr
diff --git a/src/Merge.hs b/src/Merge.hs
--- a/src/Merge.hs
+++ b/src/Merge.hs
@@ -9,25 +9,25 @@
 import Control.Exception.Base (Exception, throwIO)
 import Data.Functor ((<&>))
 import Misc
-import Printer (printExpression, printProgram)
+import Printer (printExpression)
 import Text.Printf (printf)
 
 data MergeException
-  = WrongProgramFormat Program
+  = WrongExpressionFormat Expression
   | CanNotMergeBinding Binding Binding
-  | EmptyProgramList
+  | EmptyExpressionList
   deriving (Exception)
 
 instance Show MergeException where
-  show (WrongProgramFormat prog) =
+  show (WrongExpressionFormat expr) =
     printf
-      "Invalid program format, only programs with top level formations are supported for 'merge' command, given:\n%s"
-      (printProgram prog)
+      "Invalid expression format, only expressions with top level formations are supported for 'merge' command, given:\n%s"
+      (printExpression expr)
   show (CanNotMergeBinding first second) =
     printf
       "Can't merge two bindings, conflict found:\n%s"
       (printExpression (ExFormation [first, second]))
-  show EmptyProgramList = "Nothing to merge: provide at least one program"
+  show EmptyExpressionList = "Nothing to merge: provide at least one expression"
 
 mergeBinding :: Binding -> Binding -> IO Binding
 mergeBinding first@(BiTau a (ExFormation xs)) second@(BiTau b (ExFormation ys))
@@ -47,14 +47,14 @@
   ws <- mapM (uncurry mergeBinding) collisions
   pure (xs' <> ys' <> ws)
 
-merge' :: [Program] -> IO Program
-merge' [] = throwIO EmptyProgramList
-merge' [p@(Program (ExFormation _))] = pure p
-merge' (Program (ExFormation bindings) : rest) = do
-  Program (ExFormation bds') <- merge' rest
+merge' :: [Expression] -> IO Expression
+merge' [] = throwIO EmptyExpressionList
+merge' [p@(ExFormation _)] = pure p
+merge' (ExFormation bindings : rest) = do
+  ExFormation bds' <- merge' rest
   merged <- mergeBindings bds' bindings
-  pure (Program (ExFormation merged))
-merge' (prog : _) = throwIO (WrongProgramFormat prog)
+  pure (ExFormation merged)
+merge' (expr : _) = throwIO (WrongExpressionFormat expr)
 
-merge :: [Program] -> IO Program
-merge progs = merge' (reverse progs)
+merge :: [Expression] -> IO Expression
+merge exprs = merge' (reverse exprs)
diff --git a/src/Parser.hs b/src/Parser.hs
--- a/src/Parser.hs
+++ b/src/Parser.hs
@@ -4,11 +4,9 @@
 -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 -- SPDX-License-Identifier: MIT
 
--- The goal of the module is to parse given phi program to AST
+-- The goal of the module is to parse given phi expression to AST
 module Parser
-  ( parseProgram
-  , parseProgramThrows
-  , parseExpression
+  ( parseExpression
   , parseExpressionThrows
   , parseAttribute
   , parseAttributeThrows
@@ -42,8 +40,7 @@
 type Parser = Parsec Void String
 
 data ParserException
-  = CouldNotParseProgram {message :: String}
-  | CouldNotParseExpression {message :: String}
+  = CouldNotParseExpression {message :: String}
   | CouldNotParseAttribute {message :: String}
   | CouldNotParseNumber {message :: String}
   deriving (Exception)
@@ -61,7 +58,6 @@
 phiParser = PhiParser attribute alpha index' binding expression quotedStr
 
 instance Show ParserException where
-  show CouldNotParseProgram{..} = printf "Couldn't parse given phi program, cause: %s" message
   show CouldNotParseExpression{..} = printf "Couldn't parse given phi expression, cause: %s" message
   show CouldNotParseAttribute{..} = printf "Couldn't parse given attribute, cause: %s" message
   show CouldNotParseNumber{..} = printf "Couldn't parse given number to 'Φ.number', cause: %s" message
@@ -454,21 +450,6 @@
   expr <- exHead
   exTail expr
 
-program :: Parser Program
-program =
-  choice
-    [ do
-        _ <- symbol "{"
-        prog <- Program <$> expression
-        _ <- symbol "}"
-        return prog
-    , do
-        _ <- global
-        _ <- arrow
-        Program <$> expression
-    ]
-    <?> "program"
-
 -- Entry point
 parse' :: String -> Parser a -> String -> Either String a
 parse' name parser input = do
@@ -515,9 +496,3 @@
 
 parseExpressionThrows :: String -> IO Expression
 parseExpressionThrows ex = orThrow CouldNotParseExpression (parseExpression ex)
-
-parseProgram :: String -> Either String Program
-parseProgram = parse' "program" program
-
-parseProgramThrows :: String -> IO Program
-parseProgramThrows prg = orThrow CouldNotParseProgram (parseProgram prg)
diff --git a/src/Printer.hs b/src/Printer.hs
--- a/src/Printer.hs
+++ b/src/Printer.hs
@@ -5,9 +5,7 @@
 -- SPDX-License-Identifier: MIT
 
 module Printer
-  ( printProgram
-  , printProgram'
-  , printExpression
+  ( printExpression
   , printExpression'
   , printAttribute
   , printAlpha
@@ -42,12 +40,6 @@
 
 logPrintConfig :: (SugarType, Encoding, LineFormat, Int)
 logPrintConfig = (SWEET, UNICODE, SINGLELINE, defaultMargin)
-
-printProgram' :: Program -> PrintConfig -> String
-printProgram' prog (sugar, encoding, line, margin) = T.unpack $ render (withLineFormat line $ withMargin margin $ withEncoding encoding $ withSugarType sugar $ programToCST prog)
-
-printProgram :: Program -> String
-printProgram prog = printProgram' prog defaultPrintConfig
 
 printExpression' :: Expression -> PrintConfig -> String
 printExpression' ex (sugar, encoding, line, margin) = T.unpack $ render (withLineFormat line $ withMargin margin $ withEncoding encoding $ withSugarType sugar $ expressionToCST ex)
diff --git a/src/Render.hs b/src/Render.hs
--- a/src/Render.hs
+++ b/src/Render.hs
@@ -148,10 +148,6 @@
   render TAB' = " "
   render NO_TAB = ""
 
-instance Render PROGRAM where
-  render PR_SWEET{..} = render lcb <> render space <> render expr <> render space <> render rcb
-  render PR_SALTY{..} = render global <> render SPACE <> render arrow <> render SPACE <> render expr
-
 instance Render PAIR where
   render PA_TAU{..} = render attr <> render SPACE <> render arrow <> render SPACE <> render expr
   render PA_ALPHA{..} = render alpha <> render SPACE <> render arrow <> render SPACE <> render expr
diff --git a/src/Replacer.hs b/src/Replacer.hs
--- a/src/Replacer.hs
+++ b/src/Replacer.hs
@@ -4,15 +4,12 @@
 -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 -- SPDX-License-Identifier: MIT
 
--- The goal of the module is to traverse though the Program with replacing
+-- The goal of the module is to traverse through the expression with replacing
 -- pattern sub expression with target expressions
 module Replacer
-  ( replaceProgram
-  , replaceProgramFast
-  , replaceExpression
+  ( replaceExpression
   , replaceExpressionFast
   , ReplaceContext (..)
-  , ReplaceProgramFunc
   , ReplaceExpressionFunc
   )
 where
@@ -24,8 +21,6 @@
 
 type ReplaceExpressionFunc' = ReplaceState Expression -> ReplaceContext -> ReplaceState Expression
 
-type ReplaceProgramFunc = ReplaceState Program -> Program
-
 type ReplaceExpressionFunc = ReplaceState Expression -> Expression
 
 newtype ReplaceContext = ReplaceCtx {_maxDepth :: Int}
@@ -113,9 +108,3 @@
 replaceExpressionFast ctx state =
   let (expr, _, _) = replaceExpressionFast' state ctx
    in expr
-
-replaceProgram :: ReplaceProgramFunc
-replaceProgram (Program expr, ptns, repls) = Program (replaceExpression (expr, ptns, repls))
-
-replaceProgramFast :: ReplaceContext -> ReplaceProgramFunc
-replaceProgramFast ctx (Program expr, ptns, repls) = Program (replaceExpressionFast ctx (expr, ptns, repls))
diff --git a/src/Rewriter.hs b/src/Rewriter.hs
--- a/src/Rewriter.hs
+++ b/src/Rewriter.hs
@@ -32,23 +32,23 @@
 
 type RewriteState = (NonEmpty Rewritten, Seen, Bool)
 
--- Loop-detection store. It maps a cheap fixed-size digest of a program (see
+-- Loop-detection store. It maps a cheap fixed-size digest of an expression (see
 -- 'hashExpression') to the full expressions that produced that digest. A
 -- digest collision is resolved by a slow, exact structural (==) comparison,
 -- so loops are still detected soundly while the common (no collision) case
--- stays O(1) on the digest instead of O(programSize) per lookup/insert.
+-- stays O(1) on the digest instead of O(expressionSize) per lookup/insert.
 type Seen = Map.Map Int [Expression]
 
--- Has this exact program been seen before? The digest lookup is fast; the
+-- Has this exact expression been seen before? The digest lookup is fast; the
 -- (==) check runs only on a digest match, guarding against hash collisions.
 seenMember :: Int -> Expression -> Seen -> Bool
 seenMember digest expr seen = maybe False (elem expr) (Map.lookup digest seen)
 
--- Remember a program under its digest, keeping any earlier collisions.
+-- Remember an expression under its digest, keeping any earlier collisions.
 seenInsert :: Int -> Expression -> Seen -> Seen
 seenInsert digest expr = Map.insertWith (++) digest [expr]
 
-type Rewritten = (Program, Maybe String)
+type Rewritten = (Expression, Maybe String)
 
 type Rewrittens = (NonEmpty Rewritten, Bool)
 
@@ -146,11 +146,11 @@
 tryBuildAndReplaceFast state _ = buildAndReplace' state replaceExpression
 
 -- The function returns tuple (X, Y, Z) where
--- - X is sequence of programs;
--- - Y is Set of unique programs after each rule application. It allows to stop the rewriting if we're getting
---   into loop and get back to program which we've already got before
+-- - X is sequence of expressions;
+-- - Y is Set of unique expressions after each rule application. It allows to stop the rewriting if we're getting
+--   into loop and get back to an expression which we've already got before
 -- - Z is boolean flag which tells us if we reach breakpoint. If unmatched rule is equal to breakpoint rule - entire
---   rewriting must be stopped and original program must be returned
+--   rewriting must be stopped and original expression must be returned
 rewrite' :: RewriteState -> [Y.Rule] -> Int -> RewriteContext -> IO RewriteState
 rewrite' state [] _ _ = pure state
 rewrite' state (rule : rest) iteration ctx@RewriteContext{..} = do
@@ -160,7 +160,7 @@
     _ -> rewrite' state' rest iteration ctx
   where
     _rewrite :: RewriteState -> Int -> IO RewriteState
-    _rewrite (_rewrittens@((program, _) :| _), _unique, _) _count =
+    _rewrite (_rewrittens@((current, _) :| _), _unique, _) _count =
       let ruleName = rule.name
           ptn = rule.pattern
           res = rule.result
@@ -172,7 +172,7 @@
                 else pure (_rewrittens, _unique, False)
             else do
               logDebug (printf "Starting rewriting cycle for rule '%s': %d out of %d" ruleName _count _maxDepth)
-              expression <- locatedExpression _locator program
+              expression <- locatedExpression _locator current
               R.matchExpressionWithRule expression rule (RuleContext _buildTerm) >>= \case
                 [] -> do
                   logDebug (printf "Rule '%s' does not match, rewriting is stopped" ruleName)
@@ -201,23 +201,23 @@
                                     (countNodes expr)
                                     (printExpression expr)
                                 )
-                              prog <- withLocatedExpression _locator expr program
-                              _saveStep prog (((iteration - 1) * _maxDepth) + _count)
-                              _rewrite (leadsTo prog, seenInsert digest expr _unique, False) (_count + 1)
+                              updated <- withLocatedExpression _locator expr current
+                              _saveStep updated (((iteration - 1) * _maxDepth) + _count)
+                              _rewrite (leadsTo updated, seenInsert digest expr _unique, False) (_count + 1)
       where
-        leadsTo :: Program -> NonEmpty Rewritten
-        leadsTo _prog =
-          let (program, _) :| rest = _rewrittens
-           in (_prog, Nothing) :| (program, Just rule.name) : rest
+        leadsTo :: Expression -> NonEmpty Rewritten
+        leadsTo next =
+          let (head', _) :| rest = _rewrittens
+           in (next, Nothing) :| (head', Just rule.name) : rest
 
--- Rewrite program by provided locator from RewriteContext
-rewrite :: Program -> [Y.Rule] -> RewriteContext -> IO Rewrittens
-rewrite prog rules ctx@RewriteContext{..} = do
-  (rewrittens, exceeded) <- _rewrite ((prog, Nothing) :| [], Map.empty, False) 0
+-- Rewrite the expression by provided locator from RewriteContext
+rewrite :: Expression -> [Y.Rule] -> RewriteContext -> IO Rewrittens
+rewrite expr rules ctx@RewriteContext{..} = do
+  (rewrittens, exceeded) <- _rewrite ((expr, Nothing) :| [], Map.empty, False) 0
   pure (NE.reverse rewrittens, exceeded)
   where
     _rewrite :: RewriteState -> Int -> IO Rewrittens
-    _rewrite state@(rewrittens@((program, _) :| _), _, _) count
+    _rewrite state@(rewrittens@((current, _) :| _), _, _) count
       | not (inRange _must count) && count > 0 && exceedsUpperBound _must count = throwIO (MustStopBefore _must count)
       | count == _maxCycles = do
           logDebug (printf "Max amount of rewriting cycles for all rules (%d) has been reached, rewriting is stopped" _maxCycles)
@@ -227,9 +227,9 @@
       | otherwise = do
           logDebug (printf "Starting rewriting cycle for all rules: %d out of %d" count _maxCycles)
           rewrite' state rules count ctx >>= \case
-            (_, _, True) -> pure ((prog, Nothing) :| [], False) -- breakpoint, return original program
-            state'@(rewrittens'@((program', _) :| _), _, False) ->
-              if program' == program
+            (_, _, True) -> pure ((expr, Nothing) :| [], False) -- breakpoint, return original expression
+            state'@(rewrittens'@((current', _) :| _), _, False) ->
+              if current' == current
                 then do
                   logDebug "Rewriting is stopped since it has no effect"
                   if not (inRange _must count)
diff --git a/src/Rule.hs b/src/Rule.hs
--- a/src/Rule.hs
+++ b/src/Rule.hs
@@ -6,7 +6,7 @@
 -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 -- SPDX-License-Identifier: MIT
 
-module Rule (RuleContext (..), isNF, matchProgramWithRule, matchExpressionWithRule, matchExpressionWithRule', meetCondition) where
+module Rule (RuleContext (..), isNF, matchExpressionWithRule, matchExpressionWithRule', meetCondition) where
 
 import AST
 import Builder
@@ -407,6 +407,3 @@
                       met <- meetMaybeCondition rule.having extended ctx
                       when (null met) (logDebug "The 'having' condition wasn't met")
                       pure met
-
-matchProgramWithRule :: Program -> Y.Rule -> RuleContext -> IO [Subst]
-matchProgramWithRule (Program expr) = matchExpressionWithRule expr
diff --git a/src/Sugar.hs b/src/Sugar.hs
--- a/src/Sugar.hs
+++ b/src/Sugar.hs
@@ -45,7 +45,6 @@
 --  |----------------------------|-----------------------------------------------------|
 --  | sugar                      | verbose version                                     |
 --  |----------------------------|-----------------------------------------------------|
---  | {e}                        | Q -> e                                              |
 --  | a1 -> a2                   | a1 ↦ $.a2                                           |
 --  | a -> 42                    | Q.number(Q.bytes([[ D> 40-45-00-00-00-00-00-00 ]])) |
 --  | a -> "Hey"                 | Q.number(Q.bytes([[ D> 48-65-79 ]]))                |
@@ -57,10 +56,6 @@
 class ToSalty a where
   toSalty :: a -> a
 
-instance ToSalty PROGRAM where
-  toSalty PR_SWEET{..} = PR_SALTY Φ ARROW (toSalty expr)
-  toSalty prog = prog
-
 instance ToSalty EXPRESSION where
   toSalty EX_ATTR{..} = EX_DISPATCH (EX_XI XI) NO_SPACE attr
   toSalty EX_DISPATCH{..} = EX_DISPATCH (toSalty expr) space attr
@@ -123,15 +118,21 @@
             next
             ( AA_TAUS
                 ( BI_PAIR
-                    ( PA_ALPHA
-                        (AL_IDX ALPHA 0)
+                    ( PA_TAU
+                        (AT_LABEL "as-bytes")
                         ARROW
                         ( EX_APPLICATION
                             bytes
                             NO_SPACE
                             EOL
                             (TAB (indent + 2))
-                            (AA_EXPRS (APP_ARG data' AAS_EMPTY))
+                            ( AA_TAUS
+                                ( BI_PAIR
+                                    (PA_TAU (AT_LABEL "data") ARROW data')
+                                    (BDS_EMPTY (TAB (indent + 2)))
+                                    (TAB (indent + 2))
+                                )
+                            )
                             EOL
                             next
                             (indent + 2)
diff --git a/src/Tau.hs b/src/Tau.hs
--- a/src/Tau.hs
+++ b/src/Tau.hs
@@ -27,10 +27,10 @@
 {-# NOINLINE taus #-}
 taus = unsafePerformIO (newIORef (Set.empty, 0))
 
--- Scan the program once and seed the avoid-set with every attribute label it
+-- Scan the expression once and seed the avoid-set with every attribute label it
 -- contains, resetting the cursor back to the start.
-seedTaus :: Program -> IO ()
-seedTaus (Program expr) = writeIORef taus (exprLabels expr, 0)
+seedTaus :: Expression -> IO ()
+seedTaus expr = writeIORef taus (exprLabels expr, 0)
 
 -- Mint a fresh, deterministic 𝜏-label that collides with no taken name,
 -- advancing the cursor past taken indices and recording the new name so it is
diff --git a/src/XMIR.hs b/src/XMIR.hs
--- a/src/XMIR.hs
+++ b/src/XMIR.hs
@@ -7,7 +7,7 @@
 -- SPDX-License-Identifier: MIT
 
 module XMIR
-  ( programToXMIR
+  ( expressionToXMIR
   , printXMIR
   , toName
   , parseXMIR
@@ -45,14 +45,14 @@
 data XmirContext = XmirContext
   { _omitListing :: Bool
   , _omitComments :: Bool
-  , _listing :: Program -> String
+  , _listing :: Expression -> String
   }
 
 defaultXmirContext :: XmirContext
 defaultXmirContext = XmirContext True True (const "")
 
 data XMIRException
-  = UnsupportedProgram Program
+  = UnsupportedTopExpression Expression
   | UnsupportedExpression Expression
   | UnsupportedBinding Binding
   | CouldNotParseXMIR String
@@ -60,7 +60,7 @@
   deriving (Exception)
 
 instance Show XMIRException where
-  show (UnsupportedProgram prog) = printf "XMIR does not support such program:\n%s" (printProgram prog)
+  show (UnsupportedTopExpression expr) = printf "XMIR does not support such top-level expression:\n%s" (printExpression expr)
   show (UnsupportedExpression expr) = printf "XMIR does not support such expression:\n%s" (printExpression expr)
   show (UnsupportedBinding bd) = printf "XMIR does not support such bindings: %s" (printBinding bd)
   show (CouldNotParseXMIR msg) = printf "Couldn't parse given XMIR, cause: %s" msg
@@ -103,8 +103,8 @@
 expression (DataNumber bytes) XmirContext{..} =
   let bts =
         object
-          [("as", printAlpha (Alpha 0)), ("base", "Φ.bytes")]
-          [object [] [NodeContent (T.pack (printBytes bytes))]]
+          [("as", "as-bytes"), ("base", "Φ.bytes")]
+          [object [("as", "data")] [NodeContent (T.pack (printBytes bytes))]]
    in pure
         ( "Φ.number"
         , if _omitComments
@@ -117,8 +117,8 @@
 expression (DataString bytes) XmirContext{..} =
   let bts =
         object
-          [("as", printAlpha (Alpha 0)), ("base", "Φ.bytes")]
-          [object [] [NodeContent (T.pack (printBytes bytes))]]
+          [("as", "as-bytes"), ("base", "Φ.bytes")]
+          [object [("as", "data")] [NodeContent (T.pack (printBytes bytes))]]
    in pure
         ( "Φ.string"
         , if _omitComments
@@ -163,20 +163,20 @@
 nestedBindings :: [Binding] -> XmirContext -> IO [Node]
 nestedBindings bds ctx = catMaybes <$> mapM (`formationBinding` ctx) bds
 
-programToXMIR :: Program -> XmirContext -> IO Document
-programToXMIR prog@(Program expr@(ExFormation [BiTau (AtLabel _) arg, BiVoid AtRho])) ctx@XmirContext{..} = case arg of
-  ExFormation _ -> programToXMIR'
-  ExApplication _ _ -> programToXMIR'
-  ExDispatch _ _ -> programToXMIR'
-  ExRoot -> programToXMIR'
-  _ -> throwIO (UnsupportedProgram prog)
+expressionToXMIR :: Expression -> XmirContext -> IO Document
+expressionToXMIR expr@(ExFormation [BiTau (AtLabel _) arg, BiVoid AtRho]) ctx@XmirContext{..} = case arg of
+  ExFormation _ -> expressionToXMIR'
+  ExApplication _ _ -> expressionToXMIR'
+  ExDispatch _ _ -> expressionToXMIR'
+  ExRoot -> expressionToXMIR'
+  _ -> throwIO (UnsupportedTopExpression expr)
   where
-    programToXMIR' :: IO Document
-    programToXMIR' = do
+    expressionToXMIR' :: IO Document
+    expressionToXMIR' = do
       (pckg, expr') <- getPackage expr
       root <- rootExpression expr' ctx
       now <- getCurrentTime
-      let text = _listing prog
+      let text = _listing expr
           listing =
             if _omitListing
               then show (length (lines text)) ++ " line(s)"
@@ -256,7 +256,7 @@
           fractional = realToFrac posix - fromInteger (floor posix)
           nanos = floor (fractional * 1_000_000_000) :: Int
        in base ++ "." ++ printf "%09d" nanos ++ "Z"
-programToXMIR prog _ = throwIO (UnsupportedProgram prog)
+expressionToXMIR expr _ = throwIO (UnsupportedTopExpression expr)
 
 escapeXML :: String -> String
 escapeXML = concatMap escapeChar
@@ -359,7 +359,7 @@
 parseXMIRThrows :: String -> IO Document
 parseXMIRThrows xmir = orThrow CouldNotParseXMIR (parseXMIR xmir)
 
-xmirToPhi :: Document -> IO Program
+xmirToPhi :: Document -> IO Expression
 xmirToPhi xmir =
   let doc = C.fromDocument xmir
    in case C.node doc of
@@ -377,10 +377,10 @@
                     , t <- T.splitOn "." tail'
                     ]
               if null pckg
-                then pure (Program (ExFormation [obj, BiVoid AtRho]))
+                then pure (ExFormation [obj, BiVoid AtRho])
                 else
                   let bd = foldr (\part acc -> BiTau (AtLabel (T.pack part)) (ExFormation [acc, BiLambda (Function "Package"), BiVoid AtRho])) obj pckg
-                   in pure (Program (ExFormation [bd, BiVoid AtRho]))
+                   in pure (ExFormation [bd, BiVoid AtRho])
           | otherwise -> throwIO (InvalidXMIRFormat "Expected single <object> element" doc)
         _ -> throwIO (InvalidXMIRFormat "NodeElement is expected as root element" doc)
 
diff --git a/test/ASTSpec.hs b/test/ASTSpec.hs
--- a/test/ASTSpec.hs
+++ b/test/ASTSpec.hs
@@ -5,7 +5,7 @@
 -- SPDX-License-Identifier: MIT
 
 {- | Tests for the AST module that defines the abstract syntax tree
-for phi-calculus programs including expressions, bindings, attributes, and bytes.
+for phi-calculus expressions: bindings, attributes, and bytes.
 Attention! Most of the tests are generated by LLM. Consider that when refactoring
 -}
 module ASTSpec where
@@ -200,26 +200,6 @@
       let exprs = [ExDispatch ExRoot AtRho, ExApplication ExRoot (ArTau AtRho ExRoot), ExMeta "e", ExTermination, ExRoot, ExXi, ExFormation []]
           first : _ = sort exprs
        in first `shouldBe` ExFormation []
-
-  describe "Program Eq instance compares programs" $
-    forM_
-      [ ("same programs equal", Program ExRoot, Program ExRoot, True)
-      , ("different programs differ", Program ExRoot, Program ExXi, False)
-      ]
-      ( \(desc, lhs, rhs, expected) ->
-          it desc $ (lhs == rhs) `shouldBe` expected
-      )
-
-  describe "Program Ord instance orders correctly" $
-    it "orders programs by expression" $
-      let progs = [Program ExXi, Program ExRoot, Program (ExFormation [])]
-          first : _ = sort progs
-       in first `shouldBe` Program (ExFormation [])
-
-  describe "Program Show instance renders programs" $
-    it "shows program wrapper" $
-      let hasProgram str = "Program" `elem` words str
-       in show (Program ExRoot) `shouldSatisfy` hasProgram
 
   describe "countNodes counts ExFormation with non-tau bindings" $
     forM_
diff --git a/test/CLISpec.hs b/test/CLISpec.hs
--- a/test/CLISpec.hs
+++ b/test/CLISpec.hs
@@ -120,25 +120,25 @@
 
   describe "--pin" $ do
     it "succeeds when --pin matches actual version" $
-      withStdin "Q -> [[ ]]" $
+      withStdin "[[ ]]" $
         testCLISucceeded
           ["--pin=" ++ showVersion version, "rewrite", "--sweet"]
-          ["{⟦⟧}"]
+          ["⟦⟧"]
 
     it "fails when --pin doesn't match actual version" $
-      withStdin "Q -> [[ ]]" $
+      withStdin "[[ ]]" $
         testCLIFailed
           ["--pin=9.9.9.9", "rewrite"]
           ["Version mismatch: --pin requires '9.9.9.9', but this is phino " ++ showVersion version]
 
     it "fails when --pin is empty" $
-      withStdin "Q -> [[ ]]" $
+      withStdin "[[ ]]" $
         testCLIFailed
           ["--pin=", "rewrite"]
           ["Version mismatch: --pin requires ''"]
 
   it "prints debug info with --log-level=DEBUG" $
-    withStdin "{[[]]}" $
+    withStdin "[[]]" $
       testCLISucceeded ["rewrite", "--log-level=DEBUG"] ["[DEBUG]:"]
 
   describe "rewriting" $ do
@@ -162,51 +162,51 @@
             ["--max-depth must be positive"]
 
       it "with --normalize and --must=1" $
-        withStdin "{[[ x -> [[ y -> 5 ]].y ]].x}" $
+        withStdin "[[ x -> [[ y -> 5 ]].y ]].x" $
           testCLIFailed
             ["rewrite", "--max-cycles=2", "--max-depth=1", "--normalize", "--must=1"]
             ["it's expected rewriting cycles to be in range [1], but rewriting has already reached 2"]
 
       it "when --in-place is used without input file" $
-        withStdin "Q -> [[ ]]" $
+        withStdin "[[ ]]" $
           testCLIFailed
             ["rewrite", "--in-place"]
             ["--in-place requires an input file"]
 
       it "when --in-place is used with --target" $
         withTempFile "inplaceXXXXXX.phi" $ \(path, h) -> do
-          hPutStr h "Q -> [[ ]]"
+          hPutStr h "[[ ]]"
           hClose h
           testCLIFailed
             ["rewrite", "--in-place", "--target=output.phi", path]
             ["--in-place and --target cannot be used together"]
 
       it "when --update is used without --target" $
-        withStdin "Q -> [[ ]]" $
+        withStdin "[[ ]]" $
           testCLIFailed
             ["rewrite", "--update"]
             ["--update requires --target"]
 
       it "when --update is used without an input file" $
-        withStdin "Q -> [[ ]]" $
+        withStdin "[[ ]]" $
           testCLIFailed
             ["rewrite", "--update", "--target=output.phi"]
             ["--update requires an input file"]
 
       it "when --update is used with --in-place" $
-        withStdin "Q -> [[ ]]" $
+        withStdin "[[ ]]" $
           testCLIFailed
             ["rewrite", "--update", "--in-place", "input.phi"]
             ["--update and --in-place cannot be used together"]
 
       it "with --depth-sensitive" $
-        withStdin "Q -> [[ x -> \"x\"]]" $
+        withStdin "[[ x -> \"x\"]]" $
           testCLIFailed
             ["rewrite", "--depth-sensitive", "--max-depth=1", "--max-cycles=1", rule "infinite.yaml"]
             ["[ERROR]: With option --depth-sensitive it's expected rewriting iterations amount does not reach the limit: --max-depth=1"]
 
       it "with looping rules" $
-        withStdin "Q -> [[ x -> \"0\" ]]" $
+        withStdin "[[ x -> \"0\" ]]" $
           testCLIFailed
             ["rewrite", rule "first.yaml", rule "second.yaml", "--max-depth=1", "--max-cycles=3"]
             ["it seems rewriting is looping"]
@@ -219,7 +219,7 @@
       it "with wrong attribute and valid error message" $
         testCLIFailed
           ["rewrite", resource "with-$this-attribute.phi"]
-          [ "[ERROR]: Couldn't parse given phi program, cause:"
+          [ "[ERROR]: Couldn't parse given phi expression, cause:"
           , "unexpected"
           ]
 
@@ -334,13 +334,13 @@
     it "prints help" $
       testCLISucceeded
         ["rewrite", "--help"]
-        ["Rewrite the 𝜑-program"]
+        ["Rewrite the 𝜑-expression"]
 
     it "saves steps to dir with --steps-dir" $ do
       let dir = "test-steps-temp"
       dirExists <- doesDirectoryExist dir
       when dirExists (removeDirectoryRecursive dir)
-      withStdin "Q -> [[ x -> \"hello\"]]" $ do
+      withStdin "[[ x -> \"hello\"]]" $ do
         testCLISucceeded
           ["rewrite", rule "infinite.yaml", "--max-cycles=2", "--max-depth=2", "--steps-dir=" ++ dir, "--sweet"]
           ["hello_hi_hi"]
@@ -354,18 +354,18 @@
     it "desugares without any rules flag from file" $
       testCLISucceeded
         ["rewrite", resource "desugar.phi"]
-        ["Φ ↦ ⟦ foo ↦ ξ.x, ρ ↦ ∅ ⟧"]
+        ["⟦ foo ↦ ξ.x, ρ ↦ ∅ ⟧"]
 
     it "desugares with without any rules flag from stdin" $
-      withStdin "{[[foo ↦ x]]}" $
-        testCLISucceeded ["rewrite"] ["Φ ↦ ⟦ foo ↦ ξ.x, ρ ↦ ∅ ⟧"]
+      withStdin "[[foo ↦ x]]" $
+        testCLISucceeded ["rewrite"] ["⟦ foo ↦ ξ.x, ρ ↦ ∅ ⟧"]
 
     it "rewrites with single rule" $
-      withStdin "{T(x -> Q.y)}" $
-        testCLISucceeded ["rewrite", "--rule=resources/normalize/dc.yaml"] ["Φ ↦ ⊥"]
+      withStdin "T(x -> Q.y)" $
+        testCLISucceeded ["rewrite", "--rule=resources/normalize/dc.yaml"] ["⊥"]
 
     it "fails when a rewriting rule uses a dataization-only function" $
-      withStdin "{⟦⟧}" $
+      withStdin "⟦⟧" $
         testCLIFailed
           ["rewrite", rule "evaluate-in-rewrite.yaml"]
           ["Function 'evaluate' in rule 'uses-evaluate' is available only for dataization and morphing, not for rewriting"]
@@ -374,7 +374,7 @@
       testCLISucceeded
         ["rewrite", "--normalize", resource "normalize.phi", "--margin=25"]
         [ unlines
-            [ "Φ ↦ ⟦"
+            [ "⟦"
             , "  x ↦ ⟦"
             , "    ρ ↦ ⟦"
             , "      y ↦ ⟦ ρ ↦ ∅ ⟧,"
@@ -387,11 +387,11 @@
         ]
 
     it "normalizes from stdin" $
-      withStdin "Φ ↦ ⟦ a ↦ ⟦ b ↦ ∅ ⟧ (b ↦ [[ ]]) ⟧" $
+      withStdin "⟦ a ↦ ⟦ b ↦ ∅ ⟧ (b ↦ [[ ]]) ⟧" $
         testCLISucceeded
           ["rewrite", "--normalize", "--margin=20"]
           [ unlines
-              [ "Φ ↦ ⟦"
+              [ "⟦"
               , "  a ↦ ⟦"
               , "    b ↦ ⟦ ρ ↦ ∅ ⟧,"
               , "    ρ ↦ ∅"
@@ -402,24 +402,24 @@
           ]
 
     it "rewrites with --sweet flag" $
-      withStdin "Q -> [[ x -> 5]]" $
+      withStdin "[[ x -> 5]]" $
         testCLISucceeded
           ["rewrite", "--sweet"]
-          ["{⟦ x ↦ 5 ⟧}"]
+          ["⟦ x ↦ 5 ⟧"]
 
     it "rewrites as XMIR" $
-      withStdin "Q -> [[ x -> Q.y ]]" $
+      withStdin "[[ x -> Q.y ]]" $
         testCLISucceeded
           ["rewrite", "--output=xmir"]
           ["<?xml version=\"1.0\" encoding=\"UTF-8\"?>", "<object", "  <o base=\"Φ.y\" name=\"x\"/>"]
 
     it "rewrites as LaTeX" $
-      withStdin "Q -> [[ x_o -> Q.z(y -> 5), q$ -> T, w -> $, ^ -> Q, @ -> 1, y -> \"H$@^M\", L> Fu_nc ]]" $
+      withStdin "[[ x_o -> Q.z(y -> 5), q$ -> T, w -> $, ^ -> Q, @ -> 1, y -> \"H$@^M\", L> Fu_nc ]]" $
         testCLISucceeded
           ["rewrite", "--output=latex", "--sweet"]
           [ unlines
               [ "\\begin{phiquation}"
-              , "\\Big\\{ [["
+              , "[["
               , "  |x\\char95{}o| -> Q . |z| ( |y| -> 5 ),"
               , "  |q\\char36{}| -> T,"
               , "  |w| -> \\phiTerminal{\\xi},"
@@ -427,51 +427,51 @@
               , "  @ -> 1,"
               , "  |y| -> \"H$@^M\","
               , "  L> |Fu\\char95{}nc|"
-              , "]] \\Big\\}{.}"
+              , "]]{.}"
               , "\\end{phiquation}"
               ]
           ]
 
     it "rewrites as LaTeX without numeration" $
-      withStdin "Q -> [[ x -> 5 ]]" $
+      withStdin "[[ x -> 5 ]]" $
         testCLISucceeded
           ["rewrite", "--output=latex", "--sweet", "--nonumber", "--flat"]
           [ unlines
               [ "\\begin{phiquation*}"
-              , "\\Big\\{ [[ |x| -> 5 ]] \\Big\\}{.}"
+              , "[[ |x| -> 5 ]]{.}"
               , "\\end{phiquation*}"
               ]
           ]
 
     it "rewrites an alpha-index argument as \\alpha subscript in LaTeX" $
-      withStdin "Q -> Q.foo(~1 -> Q.y)" $
+      withStdin "Q.foo(~1 -> Q.y)" $
         testCLISucceeded
           ["rewrite", "--output=latex", "--flat", "--nonumber"]
           [ unlines
               [ "\\begin{phiquation*}"
-              , "Q -> Q . |foo| ( \\phiTerminal{\\alpha_{1}} -> Q . |y| ){.}"
+              , "Q . |foo| ( \\phiTerminal{\\alpha_{1}} -> Q . |y| ){.}"
               , "\\end{phiquation*}"
               ]
           ]
 
     it "rewrite as LaTeX with expression name" $
-      withStdin "Q -> [[ x -> 5 ]]" $
+      withStdin "[[ x -> 5 ]]" $
         testCLISucceeded
           ["rewrite", "--output=latex", "--sweet", "--flat", "--expression=foo"]
           [ unlines
               [ "\\begin{phiquation}"
-              , "\\phiExpression{foo} \\Big\\{ [[ |x| -> 5 ]] \\Big\\}{.}"
+              , "\\phiExpression{foo} [[ |x| -> 5 ]]{.}"
               , "\\end{phiquation}"
               ]
           ]
 
     it "rewrite as LaTeX with label name" $
-      withStdin "Q -> [[ x -> 5 ]]" $
+      withStdin "[[ x -> 5 ]]" $
         testCLISucceeded
           ["rewrite", "--output=latex", "--sweet", "--flat", "--label=foo"]
           [ unlines
               [ "\\begin{phiquation}\n\\label{foo}"
-              , "\\Big\\{ [[ |x| -> 5 ]] \\Big\\}{.}"
+              , "[[ |x| -> 5 ]]{.}"
               , "\\end{phiquation}"
               ]
           ]
@@ -480,7 +480,7 @@
       withStdin "<object><o name=\"app\"><o name=\"x\" base=\"Φ.number\"/></o></object>" $
         testCLISucceeded
           ["rewrite", "--input=xmir", "--sweet"]
-          ["{⟦ app ↦ ⟦ x ↦ Φ.number ⟧ ⟧}"]
+          ["⟦ app ↦ ⟦ x ↦ Φ.number ⟧ ⟧"]
 
     it "rewrites and prints with XMIR as input and output" $
       withStdin
@@ -498,19 +498,19 @@
         )
 
     it "rewrites as XMIR with omit-listing flag" $
-      withStdin "Q -> [[ x -> Q.y ]]" $
+      withStdin "[[ x -> Q.y ]]" $
         testCLISucceeded
           ["rewrite", "--output=xmir", "--omit-listing"]
           ["<?xml version=\"1.0\" encoding=\"UTF-8\"?>", "<object", "<listing>1 line(s)</listing>", "  <o base=\"Φ.y\" name=\"x\"/>"]
 
     it "does not fail on exactly 1 rewriting" $
-      withStdin "{⟦ t ↦ ⟦ x ↦ \"foo\" ⟧ ⟧}" $
+      withStdin "⟦ t ↦ ⟦ x ↦ \"foo\" ⟧ ⟧" $
         testCLISucceeded
           ["rewrite", rule "simple.yaml", "--must=1", "--sweet"]
           ["x ↦ \"bar\""]
 
-    it "prints many programs with --sequence" $
-      withStdin "{[[ x -> \"foo\" ]]}" $
+    it "prints many expressions with --sequence" $
+      withStdin "[[ x -> \"foo\" ]]" $
         testCLISucceeded
           [ "rewrite"
           , rule "first.yaml"
@@ -522,14 +522,14 @@
           , "--flat"
           ]
           [ unlines
-              [ "{⟦ x ↦ \"foo\" ⟧}"
-              , "{Φ.x( y ↦ \"foo\" )}"
-              , "{⟦ x ↦ \"foo\" ⟧}"
+              [ "⟦ x ↦ \"foo\" ⟧"
+              , "Φ.x( y ↦ \"foo\" )"
+              , "⟦ x ↦ \"foo\" ⟧"
               ]
           ]
 
     it "prints only one latex preamble with --sequence" $
-      withStdin "{[[ x -> \"foo\" ]]}" $
+      withStdin "[[ x -> \"foo\" ]]" $
         testCLISucceeded
           [ "rewrite"
           , rule "first.yaml"
@@ -543,86 +543,86 @@
           ]
           [ unlines
               [ "\\begin{phiquation}"
-              , "\\Big\\{ [[ |x| -> \"foo\" ]] \\Big\\} \\leadsto_{\\nameref{r:first}}"
-              , "  \\leadsto \\Big\\{ Q . |x| ( |y| -> \"foo\" ) \\Big\\} \\leadsto_{\\nameref{r:second}}"
-              , "  \\leadsto \\Big\\{ [[ |x| -> \"foo\" ]] \\Big\\}{.}"
+              , "[[ |x| -> \"foo\" ]] \\leadsto_{\\nameref{r:first}}"
+              , "  \\leadsto Q . |x| ( |y| -> \"foo\" ) \\leadsto_{\\nameref{r:second}}"
+              , "  \\leadsto [[ |x| -> \"foo\" ]]{.}"
               , "\\end{phiquation}"
               ]
           ]
 
     it "prints meet prefix with --meet-prefix=foo in LaTeX" $
-      withStdin "{[[ x -> ?, y -> $.x ]](x -> [[ D> 42- ]]).y}" $
+      withStdin "[[ x -> ?, y -> $.x ]](x -> [[ D> 42- ]]).y" $
         testCLISucceeded
           ["rewrite", "--normalize", "--sweet", "--sequence", "--output=latex", "--flat", "--compress", "--meet-prefix=foo"]
           [ unlines
               [ "\\begin{phiquation}"
-              , "\\Big\\{ [[ |x| -> ?, |y| -> |x| ]] ( |x| -> \\phinoMeet{foo:1}{ [[ D> |42-| ]] } ) . |y| \\Big\\} \\leadsto_{\\nameref{r:copy}}"
-              , "  \\leadsto \\Big\\{ \\phinoMeet{foo:2}{ [[ |x| -> \\phinoAgain{foo:1}, |y| -> |x| ]] } . |y| \\Big\\} \\leadsto_{\\nameref{r:dot}}"
-              , "  \\leadsto \\Big\\{ \\phinoAgain{foo:2} . |x| ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:dot}}"
-              , "  \\leadsto \\Big\\{ \\phinoAgain{foo:1} ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:2}, \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:copy}}"
-              , "  \\leadsto \\Big\\{ [[ D> |42-|, \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ]] ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:stay}}"
-              , "  \\leadsto \\Big\\{ [[ D> |42-|, \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ]] \\Big\\}{.}"
+              , "[[ |x| -> ?, |y| -> |x| ]] ( |x| -> \\phinoMeet{foo:1}{ [[ D> |42-| ]] } ) . |y| \\leadsto_{\\nameref{r:copy}}"
+              , "  \\leadsto \\phinoMeet{foo:2}{ [[ |x| -> \\phinoAgain{foo:1}, |y| -> |x| ]] } . |y| \\leadsto_{\\nameref{r:dot}}"
+              , "  \\leadsto \\phinoAgain{foo:2} . |x| ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ) \\leadsto_{\\nameref{r:dot}}"
+              , "  \\leadsto \\phinoAgain{foo:1} ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:2}, \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ) \\leadsto_{\\nameref{r:copy}}"
+              , "  \\leadsto [[ D> |42-|, \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ]] ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ) \\leadsto_{\\nameref{r:stay}}"
+              , "  \\leadsto [[ D> |42-|, \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ]]{.}"
               , "\\end{phiquation}"
               ]
           ]
 
     it "prints with compressed expressions in LaTeX" $
-      withStdin "{[[ x -> ?, y -> $.x ]](x -> [[ D> 42- ]]).y}" $
+      withStdin "[[ x -> ?, y -> $.x ]](x -> [[ D> 42- ]]).y" $
         testCLISucceeded
           ["rewrite", "--normalize", "--sweet", "--sequence", "--output=latex", "--flat", "--compress"]
           [ unlines
               [ "\\begin{phiquation}"
-              , "\\Big\\{ [[ |x| -> ?, |y| -> |x| ]] ( |x| -> \\phinoMeet{1}{ [[ D> |42-| ]] } ) . |y| \\Big\\} \\leadsto_{\\nameref{r:copy}}"
-              , "  \\leadsto \\Big\\{ \\phinoMeet{2}{ [[ |x| -> \\phinoAgain{1}, |y| -> |x| ]] } . |y| \\Big\\} \\leadsto_{\\nameref{r:dot}}"
-              , "  \\leadsto \\Big\\{ \\phinoAgain{2} . |x| ( \\phiTerminal{\\rho} -> \\phinoAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:dot}}"
-              , "  \\leadsto \\Big\\{ \\phinoAgain{1} ( \\phiTerminal{\\rho} -> \\phinoAgain{2}, \\phiTerminal{\\rho} -> \\phinoAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:copy}}"
-              , "  \\leadsto \\Big\\{ [[ D> |42-|, \\phiTerminal{\\rho} -> \\phinoAgain{2} ]] ( \\phiTerminal{\\rho} -> \\phinoAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:stay}}"
-              , "  \\leadsto \\Big\\{ [[ D> |42-|, \\phiTerminal{\\rho} -> \\phinoAgain{2} ]] \\Big\\}{.}"
+              , "[[ |x| -> ?, |y| -> |x| ]] ( |x| -> \\phinoMeet{1}{ [[ D> |42-| ]] } ) . |y| \\leadsto_{\\nameref{r:copy}}"
+              , "  \\leadsto \\phinoMeet{2}{ [[ |x| -> \\phinoAgain{1}, |y| -> |x| ]] } . |y| \\leadsto_{\\nameref{r:dot}}"
+              , "  \\leadsto \\phinoAgain{2} . |x| ( \\phiTerminal{\\rho} -> \\phinoAgain{2} ) \\leadsto_{\\nameref{r:dot}}"
+              , "  \\leadsto \\phinoAgain{1} ( \\phiTerminal{\\rho} -> \\phinoAgain{2}, \\phiTerminal{\\rho} -> \\phinoAgain{2} ) \\leadsto_{\\nameref{r:copy}}"
+              , "  \\leadsto [[ D> |42-|, \\phiTerminal{\\rho} -> \\phinoAgain{2} ]] ( \\phiTerminal{\\rho} -> \\phinoAgain{2} ) \\leadsto_{\\nameref{r:stay}}"
+              , "  \\leadsto [[ D> |42-|, \\phiTerminal{\\rho} -> \\phinoAgain{2} ]]{.}"
               , "\\end{phiquation}"
               ]
           ]
 
     it "should not print \\phinoMeet{} twice" $
-      withStdin "{[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]]  ]]( y -> [[ t -> 42 ]]) ]].i ]]}" $
+      withStdin "[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]]  ]]( y -> [[ t -> 42 ]]) ]].i ]]" $
         testCLISucceeded
           ["rewrite", "--normalize", "--sequence", "--flat", "--compress", "--output=latex", "--sweet"]
           [ unlines
               [ "\\begin{phiquation}"
-              , "\\Big\\{ [[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> \\phinoMeet{1}{ [[ |t| -> 42 ]] } ]] ( |y| -> \\phinoAgain{1} ) ]] . |i| ]] \\Big\\} \\leadsto_{\\nameref{r:copy}}"
-              , "  \\leadsto \\Big\\{ [[ |ex| -> [[ |x| -> [[ |y| -> \\phinoAgain{1}, |k| -> \\phinoAgain{1} ]] ]] . |i| ]] \\Big\\} \\leadsto_{\\nameref{r:stop}}"
-              , "  \\leadsto \\Big\\{ [[ |ex| -> T ]] \\Big\\}{.}"
+              , "[[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> \\phinoMeet{1}{ [[ |t| -> 42 ]] } ]] ( |y| -> \\phinoAgain{1} ) ]] . |i| ]] \\leadsto_{\\nameref{r:copy}}"
+              , "  \\leadsto [[ |ex| -> [[ |x| -> [[ |y| -> \\phinoAgain{1}, |k| -> \\phinoAgain{1} ]] ]] . |i| ]] \\leadsto_{\\nameref{r:stop}}"
+              , "  \\leadsto [[ |ex| -> T ]]{.}"
               , "\\end{phiquation}"
               ]
           ]
 
     it "should not meet expression with high --meet-popularity" $
-      withStdin "{[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]]  ]]( y -> [[ t -> 42 ]]) ]].i ]]}" $
+      withStdin "[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]]  ]]( y -> [[ t -> 42 ]]) ]].i ]]" $
         testCLISucceeded
           ["rewrite", "--normalize", "--sequence", "--flat", "--compress", "--output=latex", "--sweet", "--meet-popularity=70"]
           [ unlines
               [ "\\begin{phiquation}"
-              , "\\Big\\{ [[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> [[ |t| -> 42 ]] ]] ( |y| -> [[ |t| -> 42 ]] ) ]] . |i| ]] \\Big\\} \\leadsto_{\\nameref{r:copy}}"
-              , "  \\leadsto \\Big\\{ [[ |ex| -> [[ |x| -> [[ |y| -> [[ |t| -> 42 ]], |k| -> [[ |t| -> 42 ]] ]] ]] . |i| ]] \\Big\\} \\leadsto_{\\nameref{r:stop}}"
-              , "  \\leadsto \\Big\\{ [[ |ex| -> T ]] \\Big\\}{.}"
+              , "[[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> [[ |t| -> 42 ]] ]] ( |y| -> [[ |t| -> 42 ]] ) ]] . |i| ]] \\leadsto_{\\nameref{r:copy}}"
+              , "  \\leadsto [[ |ex| -> [[ |x| -> [[ |y| -> [[ |t| -> 42 ]], |k| -> [[ |t| -> 42 ]] ]] ]] . |i| ]] \\leadsto_{\\nameref{r:stop}}"
+              , "  \\leadsto [[ |ex| -> T ]]{.}"
               , "\\end{phiquation}"
               ]
           ]
 
     it "meets with --meet-length=32" $
-      withStdin "{[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]]  ]]( y -> [[ t -> 42 ]]) ]].i ]]}" $
+      withStdin "[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]]  ]]( y -> [[ t -> 42 ]]) ]].i ]]" $
         testCLISucceeded
           ["rewrite", "--normalize", "--sequence", "--flat", "--compress", "--output=latex", "--sweet", "--meet-length=32"]
           [ unlines
               [ "\\begin{phiquation}"
-              , "\\Big\\{ [[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> [[ |t| -> 42 ]] ]] ( |y| -> [[ |t| -> 42 ]] ) ]] . |i| ]] \\Big\\} \\leadsto_{\\nameref{r:copy}}"
-              , "  \\leadsto \\Big\\{ [[ |ex| -> [[ |x| -> [[ |y| -> [[ |t| -> 42 ]], |k| -> [[ |t| -> 42 ]] ]] ]] . |i| ]] \\Big\\} \\leadsto_{\\nameref{r:stop}}"
-              , "  \\leadsto \\Big\\{ [[ |ex| -> T ]] \\Big\\}{.}"
+              , "[[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> [[ |t| -> 42 ]] ]] ( |y| -> [[ |t| -> 42 ]] ) ]] . |i| ]] \\leadsto_{\\nameref{r:copy}}"
+              , "  \\leadsto [[ |ex| -> [[ |x| -> [[ |y| -> [[ |t| -> 42 ]], |k| -> [[ |t| -> 42 ]] ]] ]] . |i| ]] \\leadsto_{\\nameref{r:stop}}"
+              , "  \\leadsto [[ |ex| -> T ]]{.}"
               , "\\end{phiquation}"
               ]
           ]
 
     it "focuses expression in latex with sequence" $
-      withStdin "{[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]]  ]]( y -> [[ t -> 42 ]]) ]].i ]]}" $
+      withStdin "[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]]  ]]( y -> [[ t -> 42 ]]) ]].i ]]" $
         testCLISucceeded
           ["rewrite", "--normalize", "--sequence", "--flat", "--output=latex", "--sweet", "--focus=Q.ex"]
           [ unlines
@@ -635,7 +635,7 @@
           ]
 
     it "focuses expression in latex without sequence" $
-      withStdin "{[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]]  ]]( y -> [[ t -> 42 ]]) ]].i ]]}" $
+      withStdin "[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]]  ]]( y -> [[ t -> 42 ]]) ]].i ]]" $
         testCLISucceeded
           ["rewrite", "--normalize", "--flat", "--output=latex", "--sweet", "--focus=Q.ex"]
           [ unlines
@@ -646,26 +646,26 @@
           ]
 
     it "shows exceeding of limits in latex" $
-      withStdin "{[[ x -> $.y, y -> $.x ]].x}" $
+      withStdin "[[ x -> $.y, y -> $.x ]].x" $
         testCLISucceeded
           ["rewrite", "--normalize", "--flat", "--sequence", "--output=latex", "--sweet", "--max-depth=1", "--max-cycles=1"]
           [ unlines
               [ "\\begin{phiquation}"
-              , "\\Big\\{ [[ |x| -> |y|, |y| -> |x| ]] . |x| \\Big\\} \\leadsto_{\\nameref{r:dot}}"
-              , "  \\leadsto \\Big\\{ [[ |x| -> |y|, |y| -> |x| ]] . |y| ( \\phiTerminal{\\rho} -> [[ |x| -> |y|, |y| -> |x| ]] ) \\Big\\} \\leadsto"
+              , "[[ |x| -> |y|, |y| -> |x| ]] . |x| \\leadsto_{\\nameref{r:dot}}"
+              , "  \\leadsto [[ |x| -> |y|, |y| -> |x| ]] . |y| ( \\phiTerminal{\\rho} -> [[ |x| -> |y|, |y| -> |x| ]] ) \\leadsto"
               , "  \\leadsto \\dots"
               , "\\end{phiquation}"
               ]
           ]
 
     it "focuses expression in phi without sequence" $
-      withStdin "{[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]]  ]]( y -> [[ t -> 42 ]]) ]].i ]]}" $
+      withStdin "[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]]  ]]( y -> [[ t -> 42 ]]) ]].i ]]" $
         testCLISucceeded
           ["rewrite", "--normalize", "--flat", "--output=phi", "--sweet", "--focus=Q.ex"]
           ["⊥"]
 
     it "focuses expression in phi with sequence" $
-      withStdin "{[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]]  ]]( y -> [[ t -> 42 ]]) ]].i ]]}" $
+      withStdin "[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]]  ]]( y -> [[ t -> 42 ]]) ]].i ]]" $
         testCLISucceeded
           ["rewrite", "--normalize", "--sequence", "--flat", "--output=phi", "--sweet", "--focus=Q.ex"]
           [ unlines
@@ -676,91 +676,91 @@
           ]
 
     it "prints input as listing in XMIR" $
-      withStdin "{[[ app -> [[]] ]]}" $
+      withStdin "[[ app -> [[]] ]]" $
         testCLISucceeded
           ["rewrite", "--output=xmir", "--omit-comments", "--sweet", "--flat"]
-          ["  <listing>{[[ app -> [[]] ]]}</listing>"]
+          ["  <listing>[[ app -> [[]] ]]</listing>"]
 
-    it "print program in listing in XMIRs with --sequence" $
-      withStdin "{[[ x -> \"foo\" ]]}" $
+    it "print expression in listing in XMIRs with --sequence" $
+      withStdin "[[ x -> \"foo\" ]]" $
         testCLISucceeded
           ["rewrite", "--output=xmir", "--omit-comments", "--sweet", "--flat", "--sequence", rule "simple.yaml"]
-          ["  <listing>{⟦ x ↦ \"foo\" ⟧}</listing>", "  <listing>{⟦ x ↦ \"bar\" ⟧}</listing>"]
+          ["  <listing>⟦ x ↦ \"foo\" ⟧</listing>", "  <listing>⟦ x ↦ \"bar\" ⟧</listing>"]
 
     describe "must range tests" $ do
       describe "fails" $ do
         it "when cycles exceed range ..1" $
-          withStdin "Q -> [[ x -> [[ y -> 5 ]].y ]].x" $
+          withStdin "[[ x -> [[ y -> 5 ]].y ]].x" $
             testCLIFailed
               ["rewrite", "--max-depth=1", "--max-cycles=2", "--normalize", "--must=..1"]
               ["it's expected rewriting cycles to be in range [..1], but rewriting has already reached 2"]
 
         it "when cycles below range 2.." $
-          withStdin "{⟦ t ↦ ⟦ x ↦ \"foo\" ⟧ ⟧}" $
+          withStdin "⟦ t ↦ ⟦ x ↦ \"foo\" ⟧ ⟧" $
             testCLIFailed
               ["rewrite", rule "simple.yaml", "--must=2.."]
               ["it's expected rewriting cycles to be in range [2..], but rewriting stopped after 1"]
 
         it "with invalid range 5..3" $
-          withStdin "Q -> [[ ]]" $
+          withStdin "[[ ]]" $
             testCLIFailed
               ["rewrite", "--must=5..3"]
               ["cannot parse value `5..3'"]
 
         it "with negative in range -1..5" $
-          withStdin "Q -> [[ ]]" $
+          withStdin "[[ ]]" $
             testCLIFailed
               ["rewrite", "--must=-1..5"]
               ["cannot parse value `-1..5'"]
 
         it "with malformed range syntax" $
-          withStdin "Q -> [[ ]]" $
+          withStdin "[[ ]]" $
             testCLIFailed
               ["rewrite", "--must=3...5"]
               ["cannot parse value `3...5'"]
 
       it "accepts range ..5 (0 to 5 cycles)" $
-        withStdin "Q -> [[ ]]" $
-          testCLISucceeded ["rewrite", "--must=..5", "--sweet"] ["{⟦⟧}"]
+        withStdin "[[ ]]" $
+          testCLISucceeded ["rewrite", "--must=..5", "--sweet"] ["⟦⟧"]
 
       it "accepts range 0..0 (exactly 0 cycles)" $
-        withStdin "Q -> [[ ]]" $
-          testCLISucceeded ["rewrite", "--must=0..0", "--sweet"] ["{⟦⟧}"]
+        withStdin "[[ ]]" $
+          testCLISucceeded ["rewrite", "--must=0..0", "--sweet"] ["⟦⟧"]
 
       it "accepts range 1..1 (exactly 1 cycle)" $
-        withStdin "{⟦ t ↦ ⟦ x ↦ \"foo\" ⟧ ⟧}" $
+        withStdin "⟦ t ↦ ⟦ x ↦ \"foo\" ⟧ ⟧" $
           testCLISucceeded
             ["rewrite", rule "simple.yaml", "--must=1..1", "--sweet"]
             ["x ↦ \"bar\""]
 
       it "accepts range 1..3 when 1 cycle happens" $
-        withStdin "{⟦ t ↦ ⟦ x ↦ \"foo\" ⟧ ⟧}" $
+        withStdin "⟦ t ↦ ⟦ x ↦ \"foo\" ⟧ ⟧" $
           testCLISucceeded
             ["rewrite", rule "simple.yaml", "--must=1..3", "--sweet"]
             ["x ↦ \"bar\""]
 
       it "accepts range 0.. (0 or more)" $
-        withStdin "Q -> [[ ]]" $
-          testCLISucceeded ["rewrite", "--must=0..", "--sweet"] ["{⟦⟧}"]
+        withStdin "[[ ]]" $
+          testCLISucceeded ["rewrite", "--must=0..", "--sweet"] ["⟦⟧"]
 
     it "prints to target file" $
-      withStdin "Q -> [[ ]]" $
+      withStdin "[[ ]]" $
         withTempFile "targetXXXXXX.tmp" $ \(path, h) -> do
           hClose h
           testCLISucceeded ["rewrite", "--sweet", printf "--target=%s" path] []
           content <- readFile path
-          content `shouldBe` "{⟦⟧}"
+          content `shouldBe` "⟦⟧"
 
     it "modifies file in-place" $
       withTempFile "inplaceXXXXXX.phi" $ \(path, h) -> do
-        hPutStr h "Q -> [[ x -> \"foo\" ]]"
+        hPutStr h "[[ x -> \"foo\" ]]"
         hClose h
         testCLISucceeded ["rewrite", rule "simple.yaml", "--in-place", "--sweet", path] []
         content <- readFile path
-        content `shouldBe` "{⟦ x ↦ \"bar\" ⟧}"
+        content `shouldBe` "⟦ x ↦ \"bar\" ⟧"
 
     it "skips rewriting with --update when target is newer than source" $
-      withTempFileContent "src-XXXXXX.phi" "Q -> [[ x -> \"foo\" ]]" $ \src ->
+      withTempFileContent "src-XXXXXX.phi" "[[ x -> \"foo\" ]]" $ \src ->
         withTempFileContent "tgt-XXXXXX.phi" "ORIGINAL" $ \tgt -> do
           now <- getCurrentTime
           setModificationTime src (addUTCTime (-60) now)
@@ -772,7 +772,7 @@
           content `shouldBe` "ORIGINAL"
 
     it "rewrites with --update when source is newer than target" $
-      withTempFileContent "src-XXXXXX.phi" "Q -> [[ x -> \"foo\" ]]" $ \src ->
+      withTempFileContent "src-XXXXXX.phi" "[[ x -> \"foo\" ]]" $ \src ->
         withTempFileContent "tgt-XXXXXX.phi" "ORIGINAL" $ \tgt -> do
           now <- getCurrentTime
           setModificationTime tgt (addUTCTime (-60) now)
@@ -781,54 +781,54 @@
             ["rewrite", rule "simple.yaml", "--update", "--sweet", "--target=" ++ tgt, src]
             []
           content <- readFile tgt
-          content `shouldBe` "{⟦ x ↦ \"bar\" ⟧}"
+          content `shouldBe` "⟦ x ↦ \"bar\" ⟧"
 
     it "rewrites with cycles" $
-      withStdin "Q -> [[ x -> \"x\" ]]" $
+      withStdin "[[ x -> \"x\" ]]" $
         testCLISucceeded
           ["rewrite", "--sweet", rule "infinite.yaml", "--max-depth=1", "--max-cycles=2"]
-          ["{⟦ x ↦ \"x_hi_hi\" ⟧}"]
+          ["⟦ x ↦ \"x_hi_hi\" ⟧"]
 
     it "hides default package" $
-      withStdin "{[[ org -> [[ eolang -> [[ number -> [[]] ]]]], x -> 42 ]]}" $
+      withStdin "[[ org -> [[ eolang -> [[ number -> [[]] ]]]], x -> 42 ]]" $
         testCLISucceeded
           ["rewrite", "--sweet", "--flat", "--hide=Q.org"]
-          ["{⟦ x ↦ 42 ⟧}"]
+          ["⟦ x ↦ 42 ⟧"]
 
     it "hides several FQNs" $
-      withStdin "{[[ org -> [[ eolang -> Q.x, yegor256 -> Q.y ]], x -> 42 ]]}" $
+      withStdin "[[ org -> [[ eolang -> Q.x, yegor256 -> Q.y ]], x -> 42 ]]" $
         testCLISucceeded
           ["rewrite", "--sweet", "--flat", "--hide=Q.org.eolang", "--hide=Q.org.yegor256"]
-          ["{⟦ org ↦ ⟦⟧, x ↦ 42 ⟧}"]
+          ["⟦ org ↦ ⟦⟧, x ↦ 42 ⟧"]
 
     it "shows and hides" $
-      withStdin "{[[ org -> [[ eolang -> Q.x, yegor256 -> Q.y ]], x -> 42 ]]}" $
+      withStdin "[[ org -> [[ eolang -> Q.x, yegor256 -> Q.y ]], x -> 42 ]]" $
         testCLISucceeded
           ["rewrite", "--sweet", "--flat", "--show=Q.org", "--hide=Q.org.eolang"]
-          ["{⟦ org ↦ ⟦ yegor256 ↦ Φ.y ⟧ ⟧}"]
+          ["⟦ org ↦ ⟦ yegor256 ↦ Φ.y ⟧ ⟧"]
 
     it "prints in line with --flat" $
-      withStdin "Q -> [[ x -> 5, y -> \"hey\", z -> [[ w -> [[ ]] ]] ]]" $
+      withStdin "[[ x -> 5, y -> \"hey\", z -> [[ w -> [[ ]] ]] ]]" $
         testCLISucceeded
           ["rewrite", "--sweet", "--flat"]
-          ["{⟦ x ↦ 5, y ↦ \"hey\", z ↦ ⟦ w ↦ ⟦⟧ ⟧ ⟧}"]
+          ["⟦ x ↦ 5, y ↦ \"hey\", z ↦ ⟦ w ↦ ⟦⟧ ⟧ ⟧"]
 
     it "removes unnecessary rho bindings in primitive applications" $
       withStdin
         ( unlines
-            [ "{[["
+            [ "[["
             , "  z -> [[ x -> [[ t -> 42 ]].t ]].x,"
             , "  org -> [[ eolang -> [[ bytes -> [[ data -> ? ]], number -> [[ as-bytes -> ? ]] ]] ]]"
-            , "]]}"
+            , "]]"
             ]
         )
         ( testCLISucceeded
             ["rewrite", "--sweet", "--normalize", "--flat"]
-            ["{⟦ z ↦ 42, org ↦ ⟦ eolang ↦ ⟦ bytes(data) ↦ ⟦⟧, number(as-bytes) ↦ ⟦⟧ ⟧ ⟧ ⟧}"]
+            ["⟦ z ↦ 42, org ↦ ⟦ eolang ↦ ⟦ bytes(data) ↦ ⟦⟧, number(as-bytes) ↦ ⟦⟧ ⟧ ⟧ ⟧"]
         )
 
     it "reduces log message" $
-      withStdin "{[[ x -> [[ y -> ? ]](y -> 5) ]]}" $
+      withStdin "[[ x -> [[ y -> ? ]](y -> 5) ]]" $
         testCLISucceeded
           ["rewrite", "--log-level=debug", "--log-lines=1", "--normalize"]
           [ intercalate
@@ -838,68 +838,68 @@
               ]
           ]
 
-    it "canonizes program" $
-      withStdin "{[[ x -> [[ y -> [[ L> Func ]].q, z -> Q.x(a -> [[ w -> [[ L> Atom ]], L> Hello ]]) ]], L> Package ]]}" $
+    it "canonizes expression" $
+      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 ↦ ⟦ λ ⤍ F1 ⟧.q, z ↦ Φ.x( a ↦ ⟦ w ↦ ⟦ λ ⤍ F2 ⟧, λ ⤍ F3 ⟧ ) ⟧, λ ⤍ F4 ⟧"]
 
     it "rewrites by locator" $
-      withStdin "{[[ ex -> [[ x -> [[ y -> 5 ]].y ]], abc -> [[ x -> ? ]](x -> 5) ]]}" $
+      withStdin "[[ ex -> [[ x -> [[ y -> 5 ]].y ]], abc -> [[ x -> ? ]](x -> 5) ]]" $
         testCLISucceeded
           ["rewrite", "--sweet", "--flat", "--locator=Q.ex", "--normalize"]
-          ["{⟦ ex ↦ ⟦ x ↦ 5 ⟧, abc ↦ ⟦ x ↦ ∅ ⟧( x ↦ 5 ) ⟧}"]
+          ["⟦ ex ↦ ⟦ x ↦ 5 ⟧, abc ↦ ⟦ x ↦ ∅ ⟧( x ↦ 5 ) ⟧"]
 
-    it "returns original program on --breakpoint" $
-      withStdin "{[[ x -> ?, y -> $.x ]](x -> [[ D> 42- ]]).y}" $
+    it "returns original expression on --breakpoint" $
+      withStdin "[[ x -> ?, y -> $.x ]](x -> [[ D> 42- ]]).y" $
         testCLISucceeded
           ["rewrite", "--sweet", "--flat", "--normalize", "--breakpoint=stop", "--log-level=debug"]
           [ "Applied 'copy' (30 nodes -> 25 nodes)"
           , "Rule 'stop' is a breakpoint, dropping down all the previous rewritings..."
-          , "{⟦ x ↦ ∅, y ↦ x ⟧( x ↦ ⟦ Δ ⤍ 42- ⟧ ).y}"
+          , "⟦ x ↦ ∅, y ↦ x ⟧( x ↦ ⟦ Δ ⤍ 42- ⟧ ).y"
           ]
 
   describe "dataize" $ do
     it "prints help" $
-      testCLISucceeded ["dataize", "--help"] ["Dataize the 𝜑-program"]
+      testCLISucceeded ["dataize", "--help"] ["Dataize the 𝜑-expression"]
 
-    it "dataizes simple program" $
-      withStdin "Q -> [[ D> 01- ]]" $
+    it "dataizes simple expression" $
+      withStdin "[[ D> 01- ]]" $
         testCLISucceeded ["dataize"] ["01-"]
 
     it "fails to dataize an empty object, which dataizes the terminator ⊥" $
-      withStdin "Q -> [[ ]]" $
+      withStdin "[[ ]]" $
         testCLIFailed ["dataize"] ["terminator ⊥"]
 
     it "dataizes with --sequence" $
-      withStdin "{[[ @ -> [[ x -> [[ D> 01-, y -> ? ]](y -> [[ ]]) ]].x ]]}" $
+      withStdin "[[ @ -> [[ x -> [[ D> 01-, y -> ? ]](y -> [[ ]]) ]].x ]]" $
         testCLISucceeded
           ["dataize", "--sequence", "--output=latex", "--flat", "--sweet"]
           [ intercalate
               "\n"
               [ "\\begin{phiquation}"
-              , "\\Big\\{ [[ @ -> [[ |x| -> [[ D> |01-|, |y| -> ? ]] ( |y| -> [[]] ) ]] . |x| ]] \\Big\\} \\leadsto_{\\nameref{r:contextualize}}"
-              , "  \\leadsto \\Big\\{ [[ |x| -> [[ D> |01-|, |y| -> ? ]] ( |y| -> [[]] ) ]] . |x| \\Big\\} \\leadsto_{\\nameref{r:copy}}"
-              , "  \\leadsto \\Big\\{ [[ |x| -> [[ D> |01-|, |y| -> [[]] ]] ]] . |x| \\Big\\} \\leadsto_{\\nameref{r:dot}}"
-              , "  \\leadsto \\Big\\{ [[ D> |01-|, |y| -> [[]] ]] ( \\phiTerminal{\\rho} -> [[ |x| -> [[ D> |01-|, |y| -> [[]] ]] ]] ) \\Big\\} \\leadsto_{\\nameref{r:copy}}"
-              , "  \\leadsto \\Big\\{ [[ D> |01-|, |y| -> [[]], \\phiTerminal{\\rho} -> [[ |x| -> [[ D> |01-|, |y| -> [[]] ]] ]] ]] \\Big\\}{.}"
+              , "[[ @ -> [[ |x| -> [[ D> |01-|, |y| -> ? ]] ( |y| -> [[]] ) ]] . |x| ]] \\leadsto_{\\nameref{r:contextualize}}"
+              , "  \\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| -> [[]] ]] ]] ]]{.}"
               , "\\end{phiquation}"
               , "01-"
               ]
           ]
 
     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 ]] ]] ]]}" $
+      withStdin "[[ @ -> [[ @ -> $.c.plus( 32.0 ), c -> 25.0 ]], bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus -> [[ x -> ?, L> L_number_plus ]] ]] ]]" $
         testCLISucceeded
           ["dataize", "--output=latex", "--sweet", "--nonumber", "--compress", "--canonize", "--meet-prefix=dataization", "--sequence", "--flat", "--quiet", "--hide=Q.bytes", "--hide=Q.number", "--locator=Q.@", "--focus=Q.@", "--meet-length=5", "--meet-popularity=1"]
           ["\\phinoMeet{dataization:1}{ [[ @ -> |c| . |plus| ( 32 ), |c| -> 25 ]] } \\leadsto_{\\nameref{r:contextualize}}"]
 
     it "dataizes with --locator" $
-      withStdin "{[[ ex -> [[ @ -> Q.x ]], x -> [[ D> 42- ]] ]]}" $
+      withStdin "[[ ex -> [[ @ -> Q.x ]], x -> [[ D> 42- ]] ]]" $
         testCLISucceeded ["dataize", "--locator=Q.ex"] ["42-"]
 
     it "does not print bytes with --quiet" $
-      withStdin "Q -> [[ D> 01- ]]" $
+      withStdin "[[ D> 01- ]]" $
         testCLISucceeded ["dataize", "--quiet"] []
 
     describe "fails" $ do
@@ -1092,12 +1092,14 @@
             , "\\begin{phinoMorphingInference}"
             , "  \\phinoName{mad}"
             , "  \\phinoCondition{ \\phinoNotAbsolute{ n_1 } }"
-            , "  \\phinoConclusion{ \\phinoMorph{ n ( \\tau -> n_1 ) }{ e }{ s }{ T }{ s } }"
+            , "  \\phinoPremise{ \\phinoMorph{ T }{ e }{ s_1 }{ n_2 }{ s_2 } }"
+            , "  \\phinoConclusion{ \\phinoMorph{ n ( \\tau -> n_1 ) }{ e }{ s_1 }{ n_2 }{ s_2 } }"
             , "\\end{phinoMorphingInference}"
             , "\\begin{phinoMorphingInference}"
             , "  \\phinoName{maad}"
             , "  \\phinoCondition{ \\phinoNotAbsolute{ n_1 } }"
-            , "  \\phinoConclusion{ \\phinoMorph{ n ( \\phiTerminal{\\alpha_{i}} -> n_1 ) }{ e }{ s }{ T }{ s } }"
+            , "  \\phinoPremise{ \\phinoMorph{ T }{ e }{ s_1 }{ n_2 }{ s_2 } }"
+            , "  \\phinoConclusion{ \\phinoMorph{ n ( \\phiTerminal{\\alpha_{i}} -> n_1 ) }{ e }{ s_1 }{ n_2 }{ s_2 } }"
             , "\\end{phinoMorphingInference}"
             , "\\begin{phinoMorphingInference}"
             , "  \\phinoName{universe}"
@@ -1232,16 +1234,16 @@
         )
 
   describe "merge" $ do
-    it "merges single program" $
+    it "merges single expression" $
       testCLISucceeded
         ["merge", resource "desugar.phi", "--sweet", "--flat"]
-        ["{⟦ foo ↦ x ⟧}"]
+        ["⟦ foo ↦ x ⟧"]
 
-    it "merges EO programs" $
+    it "merges EO expressions" $
       testCLISucceeded
         ["merge", "--sweet", resource "number.phi", resource "bytes.phi", resource "string.phi", "--margin=25"]
         [ unlines
-            [ "{⟦"
+            [ "⟦"
             , "  org ↦ ⟦"
             , "    eolang ↦ ⟦"
             , "      number(φ) ↦ ⟦⟧,"
@@ -1251,47 +1253,47 @@
             , "    ⟧,"
             , "    λ ⤍ Package"
             , "  ⟧"
-            , "⟧}"
+            , "⟧"
             ]
         ]
 
     it "fails on merging non formations" $
       testCLIFailed
         ["merge", resource "dispatch.phi", resource "number.phi"]
-        ["Invalid program format, only programs with top level formations are supported for 'merge' command"]
+        ["Invalid expression format, only expressions with top level formations are supported for 'merge' command"]
 
     it "fails on merging conflicted bindings" $
       testCLIFailed
         ["merge", resource "foo.phi", resource "desugar.phi"]
         ["Can't merge two bindings, conflict found"]
 
-    it "fails on merging empty list of programs" $
+    it "fails on merging empty list of expressions" $
       testCLIFailed
         ["merge"]
         ["At least one input file must be specified for 'merge' command"]
 
   describe "match" $ do
     it "takes from stdin" $
-      withStdin "{[[]]}" $
+      withStdin "[[]]" $
         testCLISucceeded ["match", "--log-level=debug"] ["[DEBUG]"]
 
     it "takes from file" $
       testCLISucceeded ["match", "test-resources/cli/foo.phi", "--log-level=debug"] ["[DEBUG]"]
 
     it "does not print substitutions without pattern" $
-      withStdin "{[[]]}" $
+      withStdin "[[]]" $
         testCLISucceeded ["match", "--log-level=debug"] ["[DEBUG]: The --pattern is not provided, no substitutions are built"]
 
     it "prints one substitution" $
-      withStdin "{[[ x -> Q.x ]]}" $
+      withStdin "[[ x -> Q.x ]]" $
         testCLISucceeded ["match", "--pattern=Q.!t"] ["t >> x"]
 
     it "prints many substitutions" $
-      withStdin "{[[ x -> Q.x, y -> Q.y ]]}" $
+      withStdin "[[ x -> Q.x, y -> Q.y ]]" $
         testCLISucceeded ["match", "--pattern=Q.!t"] ["t >> x\n------\nt >> y"]
 
     it "builds substitutions with conditions" $
-      withStdin "{[[ x -> Q.y ]].x}" $
+      withStdin "[[ x -> Q.y ]].x" $
         testCLISucceeded
           ["match", "--pattern=[[ !t -> Q.y, !B ]].!t", "--when=eq(length(!B),1)"]
           ["B >> ⟦ ρ ↦ ∅ ⟧\nt >> x"]
@@ -1302,13 +1304,13 @@
         ["B >> ⟦ foo ↦ Φ.org.eolang.x, ρ ↦ ∅ ⟧"]
 
     it "fails on parsing --when condition" $
-      withStdin "{[[]]}" $
+      withStdin "[[]]" $
         testCLIFailed
           ["match", "--pattern=[[!B]]", "--when=hello"]
           ["[ERROR]: Couldn't parse given condition"]
 
     it "fails on empty substitutions" $
-      withStdin "{Q.x.y}" $
+      withStdin "Q.x.y" $
         testCLIFailed
           ["match", "--pattern=$.!t"]
           ["[ERROR]"]
diff --git a/test/CSTSpec.hs b/test/CSTSpec.hs
--- a/test/CSTSpec.hs
+++ b/test/CSTSpec.hs
@@ -18,14 +18,14 @@
 import GHC.Generics (Generic)
 import Lining (LineFormat (SINGLELINE), withLineFormat)
 import Margin (defaultMargin, withMargin)
-import Parser (parseProgramThrows)
+import Parser (parseExpressionThrows)
 import Render (Render (render))
 import Sugar
 import System.FilePath
 import Test.Hspec
 
 data CSTPack = CSTPack
-  { program :: String
+  { expression :: String
   , result :: T.Text
   }
   deriving (Generic, Show, FromJSON)
@@ -37,27 +37,22 @@
 spec = do
   describe "builds valid CST" $
     forM_
-      [ ("Q -> Q", PR_SWEET LCB (EX_GLOBAL Φ) RCB NO_SPACE)
+      [ ("Q", EX_GLOBAL Φ)
       ,
-        ( "{[[ x -> Q.y ]]}"
-        , PR_SWEET
-            LCB
-            ( EX_FORMATION
-                LSB
-                EOL
-                (TAB 1)
-                (BI_PAIR (PA_TAU (AT_LABEL "x") ARROW (EX_DISPATCH (EX_GLOBAL Φ) NO_SPACE (AT_LABEL "y"))) (BDS_EMPTY (TAB 1)) (TAB 1))
-                EOL
-                (TAB 0)
-                RSB
-            )
-            RCB
-            NO_SPACE
+        ( "[[ x -> Q.y ]]"
+        , EX_FORMATION
+            LSB
+            EOL
+            (TAB 1)
+            (BI_PAIR (PA_TAU (AT_LABEL "x") ARROW (EX_DISPATCH (EX_GLOBAL Φ) NO_SPACE (AT_LABEL "y"))) (BDS_EMPTY (TAB 1)) (TAB 1))
+            EOL
+            (TAB 0)
+            RSB
         )
       ]
-      ( \(prog, cst) -> it prog $ do
-          ast <- parseProgramThrows prog
-          programToCST ast `shouldBe` cst
+      ( \(desc, cst) -> it desc $ do
+          ast <- parseExpressionThrows desc
+          expressionToCST ast `shouldBe` cst
       )
 
   describe "build valid CST with wrapped phinoAgain{} " $ do
@@ -87,8 +82,8 @@
       packs
       ( \pth -> it (makeRelative resources pth) $ do
           pack <- cstPack pth
-          prog <- parseProgramThrows (program pack)
-          render (withMargin defaultMargin (programToCST prog)) `shouldBe` result pack
+          parsed <- parseExpressionThrows (expression pack)
+          render (withMargin defaultMargin (expressionToCST parsed)) `shouldBe` result pack
       )
 
   describe "converts to salty CST" $ do
@@ -98,8 +93,8 @@
       packs
       ( \pth -> it (makeRelative resources pth) $ do
           pack <- cstPack pth
-          prog <- parseProgramThrows (program pack)
-          let cst = programToCST prog
+          parsed <- parseExpressionThrows (expression pack)
+          let cst = expressionToCST parsed
               salty = toSalty cst
           render salty `shouldBe` result pack
       )
@@ -111,8 +106,8 @@
       packs
       ( \pth -> it (makeRelative resources pth) $ do
           pack <- cstPack pth
-          prog <- parseProgramThrows (program pack)
-          let cst = programToCST prog
+          parsed <- parseExpressionThrows (expression pack)
+          let cst = expressionToCST parsed
               ascii = withMargin defaultMargin (withEncoding ASCII cst)
           render ascii `shouldBe` result pack
       )
@@ -124,8 +119,8 @@
       packs
       ( \pth -> it (makeRelative resources pth) $ do
           pack <- cstPack pth
-          prog <- parseProgramThrows (program pack)
-          let cst = programToCST prog
+          parsed <- parseExpressionThrows (expression pack)
+          let cst = expressionToCST parsed
               ascii = withLineFormat SINGLELINE cst
           render ascii `shouldBe` result pack
       )
diff --git a/test/DataizeSpec.hs b/test/DataizeSpec.hs
--- a/test/DataizeSpec.hs
+++ b/test/DataizeSpec.hs
@@ -16,7 +16,7 @@
 import Deps (dontSaveStep)
 import Functions (buildTerm)
 import Matcher (substEmpty)
-import Parser (parseExpressionThrows, parseProgramThrows)
+import Parser (parseExpressionThrows)
 import Rewriter (Rewritten)
 import Rule (RuleContext (RuleContext), matchExpressionWithRule')
 import Test.Hspec
@@ -32,25 +32,23 @@
 test func useCases =
   forM_ useCases $ \(desc, input, expr, output) ->
     it desc $ do
-      let prog = Program expr
-      ((res, _), _) <- func (input, (prog, Nothing) :| []) expr emptyState (defaultDataizeContext ExRoot)
+      ((res, _), _) <- func (input, (expr, Nothing) :| []) expr emptyState (defaultDataizeContext ExRoot)
       res `shouldBe` output
 
 test' :: (Eq a, Show a) => ((Expression, NonEmpty Rewritten) -> Expression -> String -> DataizeContext -> IO ((a, NonEmpty Rewritten), String)) -> [(String, Expression, Expression, a)] -> Spec
 test' func useCases =
   forM_ useCases $ \(desc, input, expr, output) ->
     it desc $ do
-      let prog = Program expr
-      ((res, _), _) <- func (input, (prog, Nothing) :| []) expr emptyState (defaultDataizeContext ExRoot)
+      ((res, _), _) <- func (input, (expr, Nothing) :| []) expr emptyState (defaultDataizeContext ExRoot)
       res `shouldBe` output
 
 testDataize :: [(String, String, String, Bytes)] -> Spec
 testDataize useCases =
-  forM_ useCases $ \(name, loc, prog, res) ->
+  forM_ useCases $ \(name, loc, src, res) ->
     it name $ do
-      prog' <- parseProgramThrows prog
+      expr <- parseExpressionThrows src
       loc' <- parseExpressionThrows loc
-      (value, _) <- dataize prog' (defaultDataizeContext loc')
+      (value, _) <- dataize expr (defaultDataizeContext loc')
       value `shouldBe` res
 
 spec :: Spec
@@ -103,8 +101,7 @@
           ]
     forM_ cases $ \(desc, input, univ, expected) ->
       it ("morphs " ++ desc ++ " to the same form across 100 random rule orders") $ do
-        let prog = Program univ
-        results <- replicateM 100 (fst . fst <$> morph (input, (prog, Nothing) :| []) univ emptyState (defaultDataizeContext ExRoot))
+        results <- replicateM 100 (fst . fst <$> morph (input, (univ, Nothing) :| []) univ emptyState (defaultDataizeContext ExRoot))
         nub results `shouldBe` [expected]
 
   -- 'md' fires only when its head is not a formation ('not (formation 𝑛)'),
@@ -132,7 +129,7 @@
     it "drills a chained λ-formation dispatch down to the base 'ml'" $ do
       let base = ExFormation [BiLambda (Function "F")]
           chain = ExDispatch (ExDispatch (ExDispatch base (AtLabel "a")) (AtLabel "b")) (AtLabel "c")
-      morph (chain, (Program ExRoot, Nothing) :| []) ExRoot emptyState (defaultDataizeContext ExRoot)
+      morph (chain, (ExRoot, Nothing) :| []) ExRoot emptyState (defaultDataizeContext ExRoot)
         `shouldThrow` (\e -> "Atom 'F' does not exist" `isInfixOf` show (e :: SomeException))
 
   -- 'norm' matches the bare meta 𝑛, which unifies with any expression, so it is
@@ -202,9 +199,8 @@
   describe "fails to dataize the terminator" $ do
     let failsOn desc input =
           it desc $
-            let prog = Program ExRoot
-             in dataize' (input, (prog, Nothing) :| []) ExRoot emptyState (defaultDataizeContext ExRoot)
-                  `shouldThrow` (\e -> "terminator" `isInfixOf` show (e :: SomeException))
+            dataize' (input, (ExRoot, Nothing) :| []) ExRoot emptyState (defaultDataizeContext ExRoot)
+              `shouldThrow` (\e -> "terminator" `isInfixOf` show (e :: SomeException))
     failsOn "throws on ⊥ instead of mapping it to empty bytes" ExTermination
     failsOn "throws on a data-less formation, which dataizes ⊥" (ExFormation [])
     -- A void slot fed a non-absolute argument morphs to ⊥ via 'mad' (#959) and
@@ -229,10 +225,10 @@
             ++ concatMap (map (verb . (.operation)) . (.premises)) Yaml.morphingRules
             ++ concatMap (map (verb . (.operation)) . (.premises)) Yaml.dataizationRules
     it "uses no step label without a defining rule or operation" $ do
-      prog <-
-        parseProgramThrows
+      expr <-
+        parseExpressionThrows
           ( unlines
-              [ "Q -> [["
+              [ "[["
               , "  bytes(data) -> [[ @ -> $.data ]],"
               , "  number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]],"
               , "  @ -> 5.plus(6)"
@@ -240,7 +236,7 @@
               ]
           )
       loc <- parseExpressionThrows "Q"
-      (_, chain) <- dataize prog (defaultDataizeContext loc)
+      (_, chain) <- dataize expr (defaultDataizeContext loc)
       let orphans = nub [label | (_, Just label) <- chain, label `notElem` allowed]
       unless
         (null orphans)
@@ -258,15 +254,15 @@
 
   describe "preserves the reduction label sequence" $ do
     let labelsOf loc src = do
-          prog <- parseProgramThrows src
+          expr <- parseExpressionThrows src
           loc' <- parseExpressionThrows loc
-          (_, chain) <- dataize prog (defaultDataizeContext loc')
+          (_, chain) <- dataize expr (defaultDataizeContext loc')
           pure [label | (_, Just label) <- chain]
     it "dataizes 5.plus(6) through the expected rules" $ do
       labels <-
         labelsOf
           "Q"
-          "Q -> [[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]"
+          "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]"
       labels
         `shouldBe` [ "contextualize"
                    , "maa"
@@ -274,8 +270,7 @@
                    , "copy"
                    , "mf"
                    , "evaluate"
-                   , "maa"
-                   , "alpha"
+                   , "ma"
                    , "copy"
                    , "mf"
                    , "contextualize"
@@ -288,15 +283,15 @@
                    , "copy"
                    ]
     it "dataizes a located reference through the expected rules" $ do
-      labels <- labelsOf "Q.foo.bar" "Q -> [[ foo -> [[ bar -> [[ @ -> Q.x ]] ]], x -> [[ D> 42- ]] ]]"
+      labels <- labelsOf "Q.foo.bar" "[[ foo -> [[ bar -> [[ @ -> Q.x ]] ]], x -> [[ D> 42- ]] ]]"
       labels `shouldBe` ["contextualize", "md", "dot", "copy", "mf"]
     -- 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).
     it "fails to dataize an empty formation, which dataizes ⊥" $ do
-      prog <- parseProgramThrows "Q -> [[ ]]"
+      expr <- parseExpressionThrows "[[ ]]"
       loc <- parseExpressionThrows "Q"
-      dataize prog (defaultDataizeContext loc)
+      dataize expr (defaultDataizeContext loc)
         `shouldThrow` (\e -> "terminator" `isInfixOf` show (e :: SomeException))
 
   testDataize
@@ -304,7 +299,7 @@
       ( "5.plus(6)"
       , "Q"
       , unlines
-          [ "Q -> [["
+          [ "[["
           , "  bytes(data) -> [["
           , "    @ -> $.data"
           , "  ]],"
@@ -321,7 +316,7 @@
       ( "Fahrenheit"
       , "Q"
       , unlines
-          [ "Q -> [["
+          [ "[["
           , "  bytes -> [["
           , "    data -> ?,"
           , "    @ -> $.data"
@@ -342,7 +337,7 @@
       ( "Factorial"
       , "Q"
       , unlines
-          [ "Q -> [["
+          [ "[["
           , "  bytes -> [["
           , "    data -> ?,"
           , "    @ -> $.data"
@@ -370,7 +365,7 @@
       ( "Located"
       , "Q.foo.bar"
       , unlines
-          [ "Q -> [["
+          [ "[["
           , "  foo -> [["
           , "    bar -> [["
           , "      @ -> Q.x"
@@ -385,7 +380,7 @@
       ( "Five"
       , "Q.x"
       , unlines
-          [ "Q -> [["
+          [ "[["
           , "  number(as-bytes) -> [[ @ -> as-bytes ]],"
           , "  bytes(data) -> [[ @ -> data ]],"
           , "  x -> 5"
diff --git a/test/FilterSpec.hs b/test/FilterSpec.hs
--- a/test/FilterSpec.hs
+++ b/test/FilterSpec.hs
@@ -7,7 +7,7 @@
 -- SPDX-License-Identifier: MIT
 
 {- | Tests for the Filter module that provides include and exclude
-functions for filtering phi-calculus programs by FQN expressions.
+functions for filtering phi-calculus expressions by FQN expressions.
 -}
 module FilterSpec where
 
@@ -20,14 +20,14 @@
 import GHC.Generics (Generic)
 import Lining (LineFormat (MULTILINE))
 import Margin (defaultMargin)
-import Parser (parseExpressionThrows, parseProgramThrows)
-import Printer (printProgram')
+import Parser (parseExpressionThrows)
+import Printer (printExpression')
 import Sugar (SugarType (SALTY))
 import System.FilePath
 import Test.Hspec
 
 data YamlPack = YamlPack
-  { program :: String
+  { expression :: String
   , shown :: [String]
   , hidden :: [String]
   , result :: String
@@ -45,20 +45,20 @@
     packs
     ( \pth -> it (makeRelative resources pth) $ do
         YamlPack{..} <- yamlPack pth
-        prog <- parseProgramThrows program
+        expr <- parseExpressionThrows expression
         included <- traverse parseExpressionThrows shown
         excluded <- traverse parseExpressionThrows hidden
-        res <- parseProgramThrows result
-        let [(prog', _)] = F.exclude (F.include [(prog, Nothing)] included) excluded
+        res <- parseExpressionThrows result
+        let [(expr', _)] = F.exclude (F.include [(expr, Nothing)] included) excluded
             cfg = (SALTY, UNICODE, MULTILINE, defaultMargin)
-        prog' `shouldBe` res
+        expr' `shouldBe` res
         when
-          (prog' /= res)
+          (expr' /= res)
           ( expectationFailure
               ( "Expected:\n"
-                  ++ printProgram' res cfg
+                  ++ printExpression' res cfg
                   ++ "\nbut got:\n"
-                  ++ printProgram' prog' cfg
+                  ++ printExpression' expr' cfg
               )
           )
     )
diff --git a/test/LaTeXSpec.hs b/test/LaTeXSpec.hs
--- a/test/LaTeXSpec.hs
+++ b/test/LaTeXSpec.hs
@@ -4,33 +4,33 @@
 -- SPDX-License-Identifier: MIT
 
 {- | Tests for the LaTeX module that provides conversion of phi-calculus
-programs and rules to LaTeX format for academic documents.
+expressions and rules to LaTeX format for academic documents.
 -}
 module LaTeXSpec where
 
 import AST (Expression (ExMeta))
 import Control.Monad (forM_)
-import LaTeX (conditionToLatex, meetInProgram)
-import Parser (parseExpressionThrows, parseProgramThrows)
+import LaTeX (conditionToLatex, meetInExpression)
+import Parser (parseExpressionThrows)
 import Test.Hspec (Spec, describe, it, shouldBe)
 import Yaml qualified as Y
 
 spec :: Spec
 spec = do
-  describe "meet program in program" $
+  describe "meet expression in expression" $
     forM_
-      [ ("Q.x.y", "{Q.x.y}", "{[[ x -> Q.x.y ]]}", ["Q.x.y"])
-      , ("Q.x.y twice", "{Q.x.y}", "{[[ x -> Q.x.y, y -> Q.x.y.z ]]}", ["Q.x.y", "Q.x.y"])
-      , ("Q.x.y.z.a and Q.x.y", "{Q.x.y.z.a}", "{[[ x -> Q.x.y, y -> Q.x.y.z ]]}", ["Q.x.y.z", "Q.x.y", "Q.x.y"])
-      , ("Ignore data objects", "{[[ x -> \"foo\" ]]}", "{Q.x( y -> \"foo\" )}", [])
-      , ("Not found [[ t -> 42 ]]", "{⟦ ex ↦ ⟦ x ↦ ⟦ t ↦ 42 ⟧.t ⟧.x ⟧}", "{⟦ ex ↦ ⟦ x ↦ 42 ⟧.x ⟧}", [])
-      , ("Missed [[ t -> 42 ]]", "{⟦ ex ↦ ⟦ x ↦ ⟦ t ↦ 42 ⟧.t ⟧.x ⟧}", "{⟦ ex ↦ 42 ⟧}", [])
+      [ ("Q.x.y", "Q.x.y", "[[ x -> Q.x.y ]]", ["Q.x.y"])
+      , ("Q.x.y twice", "Q.x.y", "[[ x -> Q.x.y, y -> Q.x.y.z ]]", ["Q.x.y", "Q.x.y"])
+      , ("Q.x.y.z.a and Q.x.y", "Q.x.y.z.a", "[[ x -> Q.x.y, y -> Q.x.y.z ]]", ["Q.x.y.z", "Q.x.y", "Q.x.y"])
+      , ("Ignore data objects", "[[ x -> \"foo\" ]]", "Q.x( y -> \"foo\" )", [])
+      , ("Not found [[ t -> 42 ]]", "⟦ ex ↦ ⟦ x ↦ ⟦ t ↦ 42 ⟧.t ⟧.x ⟧", "⟦ ex ↦ ⟦ x ↦ 42 ⟧.x ⟧", [])
+      , ("Missed [[ t -> 42 ]]", "⟦ ex ↦ ⟦ x ↦ ⟦ t ↦ 42 ⟧.t ⟧.x ⟧", "⟦ ex ↦ 42 ⟧", [])
       ]
       ( \(desc, first, second, exprs) -> it desc $ do
-          ptn <- parseProgramThrows first
-          tgt <- parseProgramThrows second
+          ptn <- parseExpressionThrows first
+          tgt <- parseExpressionThrows second
           res <- traverse parseExpressionThrows exprs
-          meetInProgram ptn 4 tgt `shouldBe` res
+          meetInExpression ptn 4 tgt `shouldBe` res
       )
 
   describe "renders the 'formation' condition" $
diff --git a/test/LocatorSpec.hs b/test/LocatorSpec.hs
--- a/test/LocatorSpec.hs
+++ b/test/LocatorSpec.hs
@@ -6,36 +6,36 @@
 import Control.Monad (forM_)
 import Data.List (intercalate)
 import Locator (locatedExpression, withLocatedExpression)
-import Parser (parseExpressionThrows, parseProgramThrows)
+import Parser (parseExpressionThrows)
 import Test.Hspec (Spec, describe, it, shouldBe)
 
 spec :: Spec
 spec = do
   describe "located expression" $
     forM_
-      [ ("{[[ x -> [[ y -> [[ z -> ? ]] ]] ]]}", "Q.x.y", "[[ z -> ? ]]")
-      , ("{[[ x -> ?, y -> [[ z -> ?, w -> [[ a -> $.x ]] ]], z -> ? ]]}", "Q.y.w.a", "$.x")
-      , ("{[[ x -> ?, y -> ? ]]}", "Q", "[[ x -> ?, y -> ? ]]")
+      [ ("[[ x -> [[ y -> [[ z -> ? ]] ]] ]]", "Q.x.y", "[[ z -> ? ]]")
+      , ("[[ x -> ?, y -> [[ z -> ?, w -> [[ a -> $.x ]] ]], z -> ? ]]", "Q.y.w.a", "$.x")
+      , ("[[ x -> ?, y -> ? ]]", "Q", "[[ x -> ?, y -> ? ]]")
       ]
-      ( \(prog, locator, res) -> it (intercalate " => " [prog, locator, res]) $ do
-          prog' <- parseProgramThrows prog
+      ( \(expr, locator, res) -> it (intercalate " => " [expr, locator, res]) $ do
+          expr' <- parseExpressionThrows expr
           locator' <- parseExpressionThrows locator
           res' <- parseExpressionThrows res
-          located <- locatedExpression locator' prog'
+          located <- locatedExpression locator' expr'
           located `shouldBe` res'
       )
 
   describe "with located expression" $
     forM_
-      [ ("{[[ x -> $ ]]}", "Q.x", "[[ y -> ? ]]", "{[[ x -> [[ y -> ? ]] ]]}")
-      , ("{[[ x -> ?, y -> [[ x -> ?, y -> [[ ]] ]] ]]}", "Q.y.y", "Q.x.y", "{[[ x -> ?, y -> [[ x -> ?, y -> Q.x.y ]] ]]}")
-      , ("{[[ x -> [[ y -> [[ z -> [[ w -> ? ]] ]] ]] ]]}", "Q.x.y", "$.a(x -> [[]])", "{[[ x -> [[ y -> $.a(x -> [[]]) ]] ]]}")
+      [ ("[[ x -> $ ]]", "Q.x", "[[ y -> ? ]]", "[[ x -> [[ y -> ? ]] ]]")
+      , ("[[ x -> ?, y -> [[ x -> ?, y -> [[ ]] ]] ]]", "Q.y.y", "Q.x.y", "[[ x -> ?, y -> [[ x -> ?, y -> Q.x.y ]] ]]")
+      , ("[[ x -> [[ y -> [[ z -> [[ w -> ? ]] ]] ]] ]]", "Q.x.y", "$.a(x -> [[]])", "[[ x -> [[ y -> $.a(x -> [[]]) ]] ]]")
       ]
-      ( \(prog, locator, expr, res) -> it (intercalate " => " [prog, locator, expr, res]) $ do
-          prog' <- parseProgramThrows prog
+      ( \(input, locator, expr, res) -> it (intercalate " => " [input, locator, expr, res]) $ do
+          input' <- parseExpressionThrows input
           locator' <- parseExpressionThrows locator
           expr' <- parseExpressionThrows expr
-          res' <- parseProgramThrows res
-          loc <- withLocatedExpression locator' expr' prog'
+          res' <- parseExpressionThrows res
+          loc <- withLocatedExpression locator' expr' input'
           loc `shouldBe` res'
       )
diff --git a/test/MergeSpec.hs b/test/MergeSpec.hs
--- a/test/MergeSpec.hs
+++ b/test/MergeSpec.hs
@@ -3,7 +3,6 @@
 
 module MergeSpec where
 
-import AST
 import Control.Monad (forM_)
 import Data.List (intercalate)
 import Merge (merge)
@@ -12,7 +11,7 @@
 
 spec :: Spec
 spec = do
-  describe "merge programs" $
+  describe "merge expressions" $
     forM_
       [
         ( ["[[ x -> 1 ]]", "[[ y -> 2 ]]"]
@@ -44,9 +43,9 @@
         )
       ]
       ( \(exprs, res) -> it res $ do
-          progs <- mapM (fmap Program . parseExpressionThrows) exprs
-          merged <- merge progs
-          res' <- fmap Program (parseExpressionThrows res)
+          parsed <- mapM parseExpressionThrows exprs
+          merged <- merge parsed
+          res' <- parseExpressionThrows res
           merged `shouldBe` res'
       )
 
@@ -57,6 +56,6 @@
       , ["[[ x -> [[ y -> Q ]] ]]", "[[ x -> [[ y -> $ ]] ]]"]
       ]
       ( \exprs -> it (intercalate " and " exprs) $ do
-          progs <- mapM (fmap Program . parseExpressionThrows) exprs
-          merge progs `shouldThrow` anyException
+          parsed <- mapM parseExpressionThrows exprs
+          merge parsed `shouldThrow` anyException
       )
diff --git a/test/ParserSpec.hs b/test/ParserSpec.hs
--- a/test/ParserSpec.hs
+++ b/test/ParserSpec.hs
@@ -28,13 +28,13 @@
 
 spec :: Spec
 spec = do
-  describe "parse program" $
+  describe "parse expression" $
     test
-      parseProgram
-      [ ("Q -> [[]]", Just (Program (ExFormation [BiVoid AtRho])))
-      , ("Q -> T(x -> Q)", Just (Program (ExApplication ExTermination (ArTau (AtLabel "x") ExRoot))))
-      , ("Q -> Q.org.eolang", Just (Program (ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "eolang"))))
-      , ("Q -> [[x -> $, y -> ?]]", Just (Program (ExFormation [BiTau (AtLabel "x") ExXi, BiVoid (AtLabel "y"), BiVoid AtRho])))
+      parseExpression
+      [ ("[[]]", Just (ExFormation [BiVoid AtRho]))
+      , ("T(x -> Q)", Just (ExApplication ExTermination (ArTau (AtLabel "x") ExRoot)))
+      , ("Q.org.eolang", Just (ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "eolang")))
+      , ("[[x -> $, y -> ?]]", Just (ExFormation [BiTau (AtLabel "x") ExXi, BiVoid (AtLabel "y"), BiVoid AtRho]))
       ]
 
   describe "parse expression" $
@@ -252,7 +252,7 @@
       packs
       ( \pack -> do
           content <- runIO (readFile pack)
-          it (takeBaseName pack) (parseProgram content `shouldSatisfy` isRight)
+          it (takeBaseName pack) (parseExpression content `shouldSatisfy` isRight)
       )
 
   describe "process typo packs" $ do
@@ -261,7 +261,7 @@
       packs
       ( \pack -> do
           content <- runIO (readFile pack)
-          it (takeBaseName pack) (parseProgram content `shouldSatisfy` isLeft)
+          it (takeBaseName pack) (parseExpression content `shouldSatisfy` isLeft)
       )
 
   describe "parse bytes" $
@@ -381,11 +381,11 @@
       , ("", Nothing)
       ]
 
-  describe "parseProgramThrows" $ do
-    it "returns program on valid input" $
-      parseProgramThrows "Q -> T" `shouldReturn` Program ExTermination
+  describe "parseExpressionThrows" $ do
+    it "returns expression on valid input" $
+      parseExpressionThrows "T" `shouldReturn` ExTermination
     it "throws on invalid input" $
-      parseProgramThrows "invalid program ]][[" `shouldThrow` anyException
+      parseExpressionThrows "invalid expression ]][[" `shouldThrow` anyException
 
   describe "parseExpressionThrows" $ do
     it "returns expression on valid input" $
diff --git a/test/PrinterSpec.hs b/test/PrinterSpec.hs
--- a/test/PrinterSpec.hs
+++ b/test/PrinterSpec.hs
@@ -80,35 +80,35 @@
             parseExpression printed `shouldBe` Right expr
       )
 
-  describe "printProgram with default config" $
+  describe "printExpression with default config" $
     forM_
-      [ ("empty formation", Program (ExFormation [BiVoid AtRho]), "{⟦⟧}")
-      , ("dispatch", Program (ExDispatch ExRoot (AtLabel "org")), "{Φ.org}")
+      [ ("empty formation", ExFormation [BiVoid AtRho], "⟦⟧")
+      , ("dispatch", ExDispatch ExRoot (AtLabel "org"), "Φ.org")
       ]
-      ( \(desc, prog, expected) ->
-          it desc (printProgram prog `shouldBe` expected)
+      ( \(desc, expr, expected) ->
+          it desc (printExpression expr `shouldBe` expected)
       )
 
-  describe "printProgram in salty does not inject a duplicate void rho when rho is already present" $
+  describe "printExpression in salty does not inject a duplicate void rho when rho is already present" $
     forM_
       [
         ( "rho bound to an empty formation"
-        , Program (ExFormation [BiTau AtRho (ExFormation [BiVoid AtRho])])
-        , "Φ ↦ ⟦ ρ ↦ ⟦ ρ ↦ ∅ ⟧ ⟧"
+        , ExFormation [BiTau AtRho (ExFormation [BiVoid AtRho])]
+        , "⟦ ρ ↦ ⟦ ρ ↦ ∅ ⟧ ⟧"
         )
       ,
         ( "rho bound to a non empty formation"
-        , Program (ExFormation [BiTau AtRho (ExFormation [BiVoid (AtLabel "名前"), BiVoid AtRho])])
-        , "Φ ↦ ⟦ ρ ↦ ⟦ 名前 ↦ ∅, ρ ↦ ∅ ⟧ ⟧"
+        , ExFormation [BiTau AtRho (ExFormation [BiVoid (AtLabel "名前"), BiVoid AtRho])]
+        , "⟦ ρ ↦ ⟦ 名前 ↦ ∅, ρ ↦ ∅ ⟧ ⟧"
         )
       ,
         ( "rho binding placed after another binding"
-        , Program (ExFormation [BiTau (AtLabel "café") ExRoot, BiTau AtRho (ExFormation [BiVoid AtRho])])
-        , "Φ ↦ ⟦ café ↦ Φ, ρ ↦ ⟦ ρ ↦ ∅ ⟧ ⟧"
+        , ExFormation [BiTau (AtLabel "café") ExRoot, BiTau AtRho (ExFormation [BiVoid AtRho])]
+        , "⟦ café ↦ Φ, ρ ↦ ⟦ ρ ↦ ∅ ⟧ ⟧"
         )
       ]
-      ( \(desc, prog, expected) ->
-          it desc (printProgram' prog (SALTY, UNICODE, SINGLELINE, defaultMargin) `shouldBe` expected)
+      ( \(desc, expr, expected) ->
+          it desc (printExpression' expr (SALTY, UNICODE, SINGLELINE, defaultMargin) `shouldBe` expected)
       )
 
   describe "printAttribute with default encoding" $
diff --git a/test/ReplacerSpec.hs b/test/ReplacerSpec.hs
--- a/test/ReplacerSpec.hs
+++ b/test/ReplacerSpec.hs
@@ -10,74 +10,68 @@
 import Replacer
 import Test.Hspec (Example (Arg), Expectation, Spec, SpecWith, describe, it, shouldBe)
 
-test :: ReplaceProgramFunc -> [(String, Program, [Expression], [Expression], Program)] -> SpecWith (Arg Expectation)
+test :: ReplaceExpressionFunc -> [(String, Expression, [Expression], [Expression], Expression)] -> SpecWith (Arg Expectation)
 test function useCases =
-  forM_ useCases $ \(desc, prog, ptns, repls, res) ->
-    it desc $ function (prog, ptns, map const repls) `shouldBe` res
+  forM_ useCases $ \(desc, expr, ptns, repls, res) ->
+    it desc $ function (expr, ptns, map const repls) `shouldBe` res
 
 spec :: Spec
 spec = do
-  describe "replace program: Program => ([Expression], [Expression]) => Program" $
+  describe "replace expression: ([Expression], [Expression]) => Expression" $
     test
-      replaceProgram
+      replaceExpression
       [
         ( "Q -> Q.y.x => ([Q.y], [$]) => Q -> $.x"
-        , Program (ExDispatch (ExDispatch ExRoot (AtLabel "y")) (AtLabel "x"))
+        , ExDispatch (ExDispatch ExRoot (AtLabel "y")) (AtLabel "x")
         , [ExDispatch ExRoot (AtLabel "y")]
         , [ExXi]
-        , Program (ExDispatch ExXi (AtLabel "x"))
+        , ExDispatch ExXi (AtLabel "x")
         )
       ,
         ( "Q -> [[x -> [[y -> $]], z -> [[w -> $]] ]] => ([[y -> $], [w -> $]], [Q.y, Q.w]) => Q -> [[x -> Q.y, z -> Q.w]]"
-        , Program
-            ( ExFormation
-                [ BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "y") ExXi])
-                , BiTau (AtLabel "z") (ExFormation [BiTau (AtLabel "w") ExXi])
-                ]
-            )
+        , ExFormation
+            [ BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "y") ExXi])
+            , BiTau (AtLabel "z") (ExFormation [BiTau (AtLabel "w") ExXi])
+            ]
         , [ExFormation [BiTau (AtLabel "y") ExXi], ExFormation [BiTau (AtLabel "w") ExXi]]
         , [ExDispatch ExRoot (AtLabel "y"), ExDispatch ExRoot (AtLabel "w")]
-        , Program
-            ( ExFormation
-                [ BiTau (AtLabel "x") (ExDispatch ExRoot (AtLabel "y"))
-                , BiTau (AtLabel "z") (ExDispatch ExRoot (AtLabel "w"))
-                ]
-            )
+        , ExFormation
+            [ BiTau (AtLabel "x") (ExDispatch ExRoot (AtLabel "y"))
+            , BiTau (AtLabel "z") (ExDispatch ExRoot (AtLabel "w"))
+            ]
         )
-      , ("Q -> [[]] => ([], [$]) => X", Program (ExFormation []), [], [ExXi], Program (ExFormation []))
+      , ("Q -> [[]] => ([], [$]) => X", ExFormation [], [], [ExXi], ExFormation [])
       ,
         ( "Q -> [[L> Func, D> 00-]] => ([ [[L> Func, D> 00-]] ], [Q]) => Q -> Q"
-        , Program (ExFormation [BiLambda (Function "Func"), BiDelta (BtOne "00")])
+        , ExFormation [BiLambda (Function "Func"), BiDelta (BtOne "00")]
         , [ExFormation [BiLambda (Function "Func"), BiDelta (BtOne "00")]]
         , [ExRoot]
-        , Program ExRoot
+        , ExRoot
         )
       ,
         ( "Q -> Q.org.eolang => ([Q.org.eolang, Q.org], [$, $]) => $"
-        , Program (ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "eolang"))
+        , ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "eolang")
         , [ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "eolang"), ExDispatch ExRoot (AtLabel "org")]
         , [ExXi, ExXi]
-        , Program ExXi
+        , ExXi
         )
       ,
         ( "Q -> [[ x -> $.t, t -> ? ]].t(^ -> [[ x -> $.t, t -> ? ]]) => ([ [[ x -> $.t, t -> ? ]].t ], [T]) => T(^ -> [[ x -> $.t, t -> ? ]])"
-        , Program
-            ( ExApplication
-                ( ExDispatch
-                    ( ExFormation
-                        [ BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t"))
-                        , BiVoid (AtLabel "t")
-                        ]
-                    )
-                    (AtLabel "t")
+        , ExApplication
+            ( ExDispatch
+                ( ExFormation
+                    [ BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t"))
+                    , BiVoid (AtLabel "t")
+                    ]
                 )
-                ( ArTau
-                    AtRho
-                    ( ExFormation
-                        [ BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t"))
-                        , BiVoid (AtLabel "t")
-                        ]
-                    )
+                (AtLabel "t")
+            )
+            ( ArTau
+                AtRho
+                ( ExFormation
+                    [ BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t"))
+                    , BiVoid (AtLabel "t")
+                    ]
                 )
             )
         ,
@@ -90,204 +84,202 @@
               (AtLabel "t")
           ]
         , [ExTermination]
-        , Program
-            ( ExApplication
-                ExTermination
-                ( ArTau
-                    AtRho
-                    ( ExFormation
-                        [ BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t"))
-                        , BiVoid (AtLabel "t")
-                        ]
-                    )
+        , ExApplication
+            ExTermination
+            ( ArTau
+                AtRho
+                ( ExFormation
+                    [ BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t"))
+                    , BiVoid (AtLabel "t")
+                    ]
                 )
             )
         )
       ,
         ( "Q -> T => ([], []) => Q -> T"
-        , Program ExTermination
+        , ExTermination
         , []
         , []
-        , Program ExTermination
+        , ExTermination
         )
       ,
         ( "Q -> $ => ([$], [Q]) => Q -> Q"
-        , Program ExXi
+        , ExXi
         , [ExXi]
         , [ExRoot]
-        , Program ExRoot
+        , ExRoot
         )
       ,
         ( "Q -> [[D> --]] => ([[D> --]], [[[L> Функція]]]) => Q -> [[L> Функція]]"
-        , Program (ExFormation [BiDelta BtEmpty])
+        , ExFormation [BiDelta BtEmpty]
         , [ExFormation [BiDelta BtEmpty]]
         , [ExFormation [BiLambda (Function "Функція")]]
-        , Program (ExFormation [BiLambda (Function "Функція")])
+        , ExFormation [BiLambda (Function "Функція")]
         )
       ,
         ( "Q -> Q.プログラム => ([Q.プログラム], [$.コード]) => Q -> $.コード"
-        , Program (ExDispatch ExRoot (AtLabel "プログラム"))
+        , ExDispatch ExRoot (AtLabel "プログラム")
         , [ExDispatch ExRoot (AtLabel "プログラム")]
         , [ExDispatch ExXi (AtLabel "コード")]
-        , Program (ExDispatch ExXi (AtLabel "コード"))
+        , ExDispatch ExXi (AtLabel "コード")
         )
       ,
         ( "Q -> [[^ -> T, @ -> T]] => ([T, T], [Q, $]) => Q -> [[^ -> Q, @ -> $]]"
-        , Program (ExFormation [BiTau AtRho ExTermination, BiTau AtPhi ExTermination])
+        , ExFormation [BiTau AtRho ExTermination, BiTau AtPhi ExTermination]
         , [ExTermination, ExTermination]
         , [ExRoot, ExXi]
-        , Program (ExFormation [BiTau AtRho ExRoot, BiTau AtPhi ExXi])
+        , ExFormation [BiTau AtRho ExRoot, BiTau AtPhi ExXi]
         )
       ,
         ( "Q -> [[x -> [[y -> Q]]]].x => ([[y -> Q]], [[[z -> $]]]) => Q -> [[x -> [[z -> $]]]].x"
-        , Program (ExDispatch (ExFormation [BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "y") ExRoot])]) (AtLabel "x"))
+        , ExDispatch (ExFormation [BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "y") ExRoot])]) (AtLabel "x")
         , [ExFormation [BiTau (AtLabel "y") ExRoot]]
         , [ExFormation [BiTau (AtLabel "z") ExXi]]
-        , Program (ExDispatch (ExFormation [BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "z") ExXi])]) (AtLabel "x"))
+        , ExDispatch (ExFormation [BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "z") ExXi])]) (AtLabel "x")
         )
       ,
         ( "Q -> Q.a(b -> Q.c) => ([Q.a, Q.c], [$, T]) => Q -> $(b -> T)"
-        , Program (ExApplication (ExDispatch ExRoot (AtLabel "a")) (ArTau (AtLabel "b") (ExDispatch ExRoot (AtLabel "c"))))
+        , ExApplication (ExDispatch ExRoot (AtLabel "a")) (ArTau (AtLabel "b") (ExDispatch ExRoot (AtLabel "c")))
         , [ExDispatch ExRoot (AtLabel "a"), ExDispatch ExRoot (AtLabel "c")]
         , [ExXi, ExTermination]
-        , Program (ExApplication ExXi (ArTau (AtLabel "b") ExTermination))
+        , ExApplication ExXi (ArTau (AtLabel "b") ExTermination)
         )
       ,
         ( "Q -> [[D> 00-01-02-]] => ([[D> 00-01-02-]], [[[D> FF-]]]) => Q -> [[D> FF-]]"
-        , Program (ExFormation [BiDelta (BtMany ["00", "01", "02"])])
+        , ExFormation [BiDelta (BtMany ["00", "01", "02"])]
         , [ExFormation [BiDelta (BtMany ["00", "01", "02"])]]
         , [ExFormation [BiDelta (BtOne "FF")]]
-        , Program (ExFormation [BiDelta (BtOne "FF")])
+        , ExFormation [BiDelta (BtOne "FF")]
         )
       ,
         ( "Q -> [[@ -> $.x, ^ -> $.y]] => ([$.x, $.y], [T, Q]) => Q -> [[@ -> T, ^ -> Q]]"
-        , Program (ExFormation [BiTau AtPhi (ExDispatch ExXi (AtLabel "x")), BiTau AtRho (ExDispatch ExXi (AtLabel "y"))])
+        , ExFormation [BiTau AtPhi (ExDispatch ExXi (AtLabel "x")), BiTau AtRho (ExDispatch ExXi (AtLabel "y"))]
         , [ExDispatch ExXi (AtLabel "x"), ExDispatch ExXi (AtLabel "y")]
         , [ExTermination, ExRoot]
-        , Program (ExFormation [BiTau AtPhi ExTermination, BiTau AtRho ExRoot])
+        , ExFormation [BiTau AtPhi ExTermination, BiTau AtRho ExRoot]
         )
       ,
         ( "Q -> Q.a.b.c => ([Q.a.b.c, Q.a.b, Q.a], [$, T, Q]) => Q -> $"
-        , Program (ExDispatch (ExDispatch (ExDispatch ExRoot (AtLabel "a")) (AtLabel "b")) (AtLabel "c"))
+        , ExDispatch (ExDispatch (ExDispatch ExRoot (AtLabel "a")) (AtLabel "b")) (AtLabel "c")
         ,
           [ ExDispatch (ExDispatch (ExDispatch ExRoot (AtLabel "a")) (AtLabel "b")) (AtLabel "c")
           , ExDispatch (ExDispatch ExRoot (AtLabel "a")) (AtLabel "b")
           , ExDispatch ExRoot (AtLabel "a")
           ]
         , [ExXi, ExTermination, ExRoot]
-        , Program ExXi
+        , ExXi
         )
       ]
 
-  describe "replace program fast: Program => ([Expression], [Expression]) => Program" $
+  describe "replace expression fast: ([Expression], [Expression]) => Expression" $
     test
-      (replaceProgramFast (ReplaceCtx 3))
+      (replaceExpressionFast (ReplaceCtx 3))
       [
         ( "Q -> [[^ -> ?, @ -> ?, D> -> ?]] => [[ !B1, !t -> ?, !B2 ]] => [[ !B1, !t -> $, !B2 ]] => Q -> [[ ^ -> $, @ -> $, D> -> $ ]]"
-        , Program (ExFormation [BiVoid AtRho, BiVoid AtPhi, BiVoid AtDelta])
+        , ExFormation [BiVoid AtRho, BiVoid AtPhi, BiVoid AtDelta]
         , [ExFormation [BiVoid AtRho], ExFormation [BiVoid AtPhi], ExFormation [BiVoid AtDelta]]
         , [ExFormation [BiTau AtRho ExXi], ExFormation [BiTau AtPhi ExXi], ExFormation [BiTau AtDelta ExXi]]
-        , Program (ExFormation [BiTau AtRho ExXi, BiTau AtPhi ExXi, BiTau AtDelta ExXi])
+        , ExFormation [BiTau AtRho ExXi, BiTau AtPhi ExXi, BiTau AtDelta ExXi]
         )
       ,
         ( "Q -> [[ ^ -> ? ]] => [[ !B1, !t -> ?, !B2 ]] => [[ !B1, !t -> [[ !t -> ? ]], !B2 ]] => Q -> [[ ^ -> [[ ^ -> [[ ^ -> [[ ^ -> ? ]] ]] ]] ]]"
-        , Program (ExFormation [BiVoid AtRho])
+        , ExFormation [BiVoid AtRho]
         , [ExFormation [BiVoid AtRho]]
         , [ExFormation [BiTau AtRho (ExFormation [BiVoid AtRho])]]
-        , Program (ExFormation [BiTau AtRho (ExFormation [BiTau AtRho (ExFormation [BiTau AtRho (ExFormation [BiVoid AtRho])])])])
+        , ExFormation [BiTau AtRho (ExFormation [BiTau AtRho (ExFormation [BiTau AtRho (ExFormation [BiVoid AtRho])])])]
         )
       ,
         ( "Q -> [[ ^ -> T ]](^ -> [[ ^ -> $]]).@ => [[ !B1, !t -> ?, !B2 ]] => [[ !B1, !t -> $, !B2 ]] => Q -> [[ ^ -> $ ]].@"
-        , Program (ExDispatch (ExApplication (ExFormation [BiTau AtRho ExTermination]) (ArTau AtRho (ExFormation [BiTau AtRho ExXi]))) AtPhi)
+        , ExDispatch (ExApplication (ExFormation [BiTau AtRho ExTermination]) (ArTau AtRho (ExFormation [BiTau AtRho ExXi]))) AtPhi
         , [ExFormation [BiTau AtRho ExTermination], ExFormation [BiTau AtRho ExXi]]
         , [ExFormation [BiTau AtRho ExRoot], ExFormation [BiVoid AtPhi]]
-        , Program (ExDispatch (ExApplication (ExFormation [BiTau AtRho ExRoot]) (ArTau AtRho (ExFormation [BiVoid AtPhi]))) AtPhi)
+        , ExDispatch (ExApplication (ExFormation [BiTau AtRho ExRoot]) (ArTau AtRho (ExFormation [BiVoid AtPhi]))) AtPhi
         )
       ,
         ( "Q -> [[ ]] => ([], []) => Q -> [[ ]]"
-        , Program (ExFormation [])
+        , ExFormation []
         , []
         , []
-        , Program (ExFormation [])
+        , ExFormation []
         )
       ,
         ( "Q -> $ => ([$], [T]) => Q -> $"
-        , Program ExXi
+        , ExXi
         , [ExXi]
         , [ExTermination]
-        , Program ExXi
+        , ExXi
         )
       ,
         ( "Q -> [[ a -> ?, b -> ?, c -> ? ]] => ([[a -> ?]], [[a -> Q]]) => Q -> [[a -> Q, b -> ?, c -> ?]]"
-        , Program (ExFormation [BiVoid (AtLabel "a"), BiVoid (AtLabel "b"), BiVoid (AtLabel "c")])
+        , ExFormation [BiVoid (AtLabel "a"), BiVoid (AtLabel "b"), BiVoid (AtLabel "c")]
         , [ExFormation [BiVoid (AtLabel "a")]]
         , [ExFormation [BiTau (AtLabel "a") ExRoot]]
-        , Program (ExFormation [BiTau (AtLabel "a") ExRoot, BiVoid (AtLabel "b"), BiVoid (AtLabel "c")])
+        , ExFormation [BiTau (AtLabel "a") ExRoot, BiVoid (AtLabel "b"), BiVoid (AtLabel "c")]
         )
       ,
         ( "Q -> [[ λ -> ?, D> 00- ]] => ([[λ -> ?]], [[λ -> $]]) => Q -> [[λ -> $, D> 00-]]"
-        , Program (ExFormation [BiVoid AtLambda, BiDelta (BtOne "00")])
+        , ExFormation [BiVoid AtLambda, BiDelta (BtOne "00")]
         , [ExFormation [BiVoid AtLambda]]
         , [ExFormation [BiTau AtLambda ExXi]]
-        , Program (ExFormation [BiTau AtLambda ExXi, BiDelta (BtOne "00")])
+        , ExFormation [BiTau AtLambda ExXi, BiDelta (BtOne "00")]
         )
       ,
         ( "Q -> [[x -> [[y -> ?]]]].x => ([[y -> ?]], [[y -> Q]]) => Q -> [[x -> [[y -> Q]]]].x"
-        , Program (ExDispatch (ExFormation [BiTau (AtLabel "x") (ExFormation [BiVoid (AtLabel "y")])]) (AtLabel "x"))
+        , ExDispatch (ExFormation [BiTau (AtLabel "x") (ExFormation [BiVoid (AtLabel "y")])]) (AtLabel "x")
         , [ExFormation [BiVoid (AtLabel "y")]]
         , [ExFormation [BiTau (AtLabel "y") ExRoot]]
-        , Program (ExDispatch (ExFormation [BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "y") ExRoot])]) (AtLabel "x"))
+        , ExDispatch (ExFormation [BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "y") ExRoot])]) (AtLabel "x")
         )
       ,
         ( "Q -> [[アイテム -> ?]] => ([[アイテム -> ?]], [[アイテム -> $]]) => Q -> [[アイテム -> $]]"
-        , Program (ExFormation [BiVoid (AtLabel "アイテム")])
+        , ExFormation [BiVoid (AtLabel "アイテム")]
         , [ExFormation [BiVoid (AtLabel "アイテム")]]
         , [ExFormation [BiTau (AtLabel "アイテム") ExXi]]
-        , Program (ExFormation [BiTau (AtLabel "アイテム") ExXi])
+        , ExFormation [BiTau (AtLabel "アイテム") ExXi]
         )
       ,
         ( "Q -> [[a -> ?, a -> ?]] => ([[a -> ?]], [[a -> Q]]) => Q -> [[a -> Q, a -> Q]]"
-        , Program (ExFormation [BiVoid (AtLabel "a"), BiVoid (AtLabel "a")])
+        , ExFormation [BiVoid (AtLabel "a"), BiVoid (AtLabel "a")]
         , [ExFormation [BiVoid (AtLabel "a")]]
         , [ExFormation [BiTau (AtLabel "a") ExRoot]]
-        , Program (ExFormation [BiTau (AtLabel "a") ExRoot, BiTau (AtLabel "a") ExRoot])
+        , ExFormation [BiTau (AtLabel "a") ExRoot, BiTau (AtLabel "a") ExRoot]
         )
       ,
         ( "Q -> Q.a(b -> [[c -> ?]]) => ([[c -> ?]], [[c -> T]]) => Q -> Q.a(b -> [[c -> T]])"
-        , Program (ExApplication (ExDispatch ExRoot (AtLabel "a")) (ArTau (AtLabel "b") (ExFormation [BiVoid (AtLabel "c")])))
+        , ExApplication (ExDispatch ExRoot (AtLabel "a")) (ArTau (AtLabel "b") (ExFormation [BiVoid (AtLabel "c")]))
         , [ExFormation [BiVoid (AtLabel "c")]]
         , [ExFormation [BiTau (AtLabel "c") ExTermination]]
-        , Program (ExApplication (ExDispatch ExRoot (AtLabel "a")) (ArTau (AtLabel "b") (ExFormation [BiTau (AtLabel "c") ExTermination])))
+        , ExApplication (ExDispatch ExRoot (AtLabel "a")) (ArTau (AtLabel "b") (ExFormation [BiTau (AtLabel "c") ExTermination]))
         )
       ,
         ( "Q -> [[ L> Функція ]] => ([[ L> Функція ]], [[ L> Код ]]) => Q -> [[ L> Код ]]"
-        , Program (ExFormation [BiLambda (Function "Функція")])
+        , ExFormation [BiLambda (Function "Функція")]
         , [ExFormation [BiLambda (Function "Функція")]]
         , [ExFormation [BiLambda (Function "Код")]]
-        , Program (ExFormation [BiLambda (Function "Код")])
+        , ExFormation [BiLambda (Function "Код")]
         )
       ]
 
-  describe "replace program fast with depth 0" $
+  describe "replace expression fast with depth 0" $
     test
-      (replaceProgramFast (ReplaceCtx 0))
+      (replaceExpressionFast (ReplaceCtx 0))
       [
         ( "Q -> [[a -> ?]] => ([[a -> ?]], [[a -> $]]) => Q -> [[a -> ?]]"
-        , Program (ExFormation [BiVoid (AtLabel "a")])
+        , ExFormation [BiVoid (AtLabel "a")]
         , [ExFormation [BiVoid (AtLabel "a")]]
         , [ExFormation [BiTau (AtLabel "a") ExXi]]
-        , Program (ExFormation [BiVoid (AtLabel "a")])
+        , ExFormation [BiVoid (AtLabel "a")]
         )
       ]
 
-  describe "replace program fast with depth 1" $
+  describe "replace expression fast with depth 1" $
     test
-      (replaceProgramFast (ReplaceCtx 1))
+      (replaceExpressionFast (ReplaceCtx 1))
       [
         ( "Q -> [[ ^ -> ? ]] => [[ ^ -> ? ]] => [[ ^ -> [[ ^ -> ? ]] ]] => Q -> [[ ^ -> [[ ^ -> ? ]] ]]"
-        , Program (ExFormation [BiVoid AtRho])
+        , ExFormation [BiVoid AtRho]
         , [ExFormation [BiVoid AtRho]]
         , [ExFormation [BiTau AtRho (ExFormation [BiVoid AtRho])]]
-        , Program (ExFormation [BiTau AtRho (ExFormation [BiVoid AtRho])])
+        , ExFormation [BiTau AtRho (ExFormation [BiVoid AtRho])]
         )
       ]
diff --git a/test/RewriterSpec.hs b/test/RewriterSpec.hs
--- a/test/RewriterSpec.hs
+++ b/test/RewriterSpec.hs
@@ -19,8 +19,8 @@
 import Functions (buildTerm)
 import GHC.Generics
 import Must (Must (..))
-import Parser (parseProgramThrows)
-import Printer (printProgram)
+import Parser (parseExpressionThrows)
+import Printer (printExpression)
 import Rewriter (RewriteContext (RewriteContext), rewrite)
 import System.FilePath (makeRelative, replaceExtension, (</>))
 import Tau (seedTaus)
@@ -84,8 +84,8 @@
           case skip pack of
             Just True -> pending
             _ -> do
-              prog <- parseProgramThrows (input pack)
-              seedTaus prog
+              expr <- parseExpressionThrows (input pack)
+              seedTaus expr
               rules' <- case rules pack of
                 Just _rules -> case custom _rules of
                   Just custom' -> pure custom'
@@ -104,7 +104,7 @@
                     else pure []
               (rewrittens, _) <-
                 rewrite
-                  prog
+                  expr
                   rules'
                   ( RewriteContext
                       ExRoot
@@ -116,13 +116,13 @@
                       Nothing
                       dontSaveStep
                   )
-              let (program, _) = NE.last rewrittens
-              result' <- parseProgramThrows (output pack)
-              unless (program == result') $
+              let (rewritten, _) = NE.last rewrittens
+              result' <- parseExpressionThrows (output pack)
+              unless (rewritten == result') $
                 expectationFailure
-                  ( "Wrong rewritten program. Expected:\n"
-                      ++ printProgram result'
+                  ( "Wrong rewritten expression. Expected:\n"
+                      ++ printExpression result'
                       ++ "\nGot:\n"
-                      ++ printProgram program
+                      ++ printExpression rewritten
                   )
       )
diff --git a/test/RuleSpec.hs b/test/RuleSpec.hs
--- a/test/RuleSpec.hs
+++ b/test/RuleSpec.hs
@@ -7,7 +7,7 @@
 
 module RuleSpec where
 
-import AST (Argument (..), Attribute (..), Binding (..), Bytes (..), Expression (..), Function (..), Program (Program))
+import AST (Argument (..), Attribute (..), Binding (..), Bytes (..), Expression (..), Function (..))
 import Control.Monad
 import Data.Aeson
 import Data.Yaml qualified as Y
@@ -38,8 +38,8 @@
       packs
       ( \pth -> it (makeRelative resources pth) $ do
           pack <- Y.decodeFileThrow pth :: IO ConditionPack
-          let prog = Program (expression pack)
-          let matched = matchProgram (pattern pack) prog
+          let expr = expression pack
+          let matched = matchExpression (pattern pack) expr
           unless (matched /= []) (expectationFailure "List of matched substitutions is empty which is not expected")
           met <- meetCondition (condition pack) matched (RuleContext buildTerm)
           case failure pack of
diff --git a/test/TauSpec.hs b/test/TauSpec.hs
--- a/test/TauSpec.hs
+++ b/test/TauSpec.hs
@@ -13,23 +13,21 @@
 spec :: Spec
 spec = describe "Tau" $ do
   it "mints sequential names after seeding from an empty document" $ do
-    seedTaus (Program (ExFormation []))
+    seedTaus (ExFormation [])
     names <- replicateM 3 freshTau
     names `shouldBe` ["a🌵0", "a🌵1", "a🌵2"]
   it "resets the cursor on every seeding so output is deterministic" $ do
-    seedTaus (Program (ExFormation []))
+    seedTaus (ExFormation [])
     first <- freshTau
-    seedTaus (Program (ExFormation []))
+    seedTaus (ExFormation [])
     second <- freshTau
     (first, second) `shouldBe` ("a🌵0", "a🌵0")
   it "skips names already taken in the document" $ do
     seedTaus
-      ( Program
-          ( ExFormation
-              [ BiTau (AtLabel "a🌵0") ExRoot
-              , BiTau (AtLabel "a🌵2") ExRoot
-              ]
-          )
+      ( ExFormation
+          [ BiTau (AtLabel "a🌵0") ExRoot
+          , BiTau (AtLabel "a🌵2") ExRoot
+          ]
       )
     names <- replicateM 2 freshTau
     names `shouldBe` ["a🌵1", "a🌵3"]
diff --git a/test/XMIRSpec.hs b/test/XMIRSpec.hs
--- a/test/XMIRSpec.hs
+++ b/test/XMIRSpec.hs
@@ -8,7 +8,6 @@
 
 module XMIRSpec where
 
-import AST
 import Control.Monad (forM_, unless)
 import Data.Aeson
 import Data.Char (isDigit)
@@ -17,12 +16,12 @@
 import Data.Yaml qualified as Yaml
 import Files (allPathsIn)
 import GHC.Generics (Generic)
-import Parser (parseExpressionThrows, parseProgramThrows)
+import Parser (parseExpressionThrows)
 import System.FilePath (makeRelative)
 import Test.Hspec (Spec, anyException, describe, expectationFailure, it, runIO, shouldBe, shouldThrow)
 import Text.XML (Document (..), Element (..))
 import Text.XML.Cursor qualified as C
-import XMIR (defaultXmirContext, parseXMIRThrows, printXMIR, programToXMIR, toName, xmirToPhi)
+import XMIR (defaultXmirContext, expressionToXMIR, parseXMIRThrows, printXMIR, toName, xmirToPhi)
 
 data ParsePack = ParsePack
   { failure :: Maybe Bool
@@ -202,7 +201,7 @@
             Just True -> xmir' `shouldThrow` anyException
             _ -> do
               xmir'' <- xmir'
-              phi'' <- parseProgramThrows phi'
+              phi'' <- parseExpressionThrows phi'
               xmir'' `shouldBe` phi''
       )
 
@@ -219,7 +218,7 @@
       ]
       ( \phi' -> it phi' $ do
           expr <- parseExpressionThrows phi'
-          programToXMIR (Program expr) defaultXmirContext `shouldThrow` anyException
+          expressionToXMIR expr defaultXmirContext `shouldThrow` anyException
       )
 
   describe "XMIR printing packs" $ do
@@ -231,8 +230,8 @@
           it (makeRelative resources pth) $ do
             pack <- printPack pth
             let PrintPack{phi = phi', xpaths = xpaths'} = pack
-            prog <- parseProgramThrows phi'
-            xmir' <- programToXMIR prog defaultXmirContext
+            expr <- parseExpressionThrows phi'
+            xmir' <- expressionToXMIR expr defaultXmirContext
             let failed = filter (not . matches xmir') xpaths'
             unless
               (null failed)