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.0.50
+version: 0.0.0.51
 license: MIT
 synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions
 description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
@@ -34,6 +34,7 @@
   exposed-modules:
     AST
     Builder
+    Canonizer
     CLI
     Condition
     CST
diff --git a/src/CLI.hs b/src/CLI.hs
--- a/src/CLI.hs
+++ b/src/CLI.hs
@@ -10,6 +10,7 @@
 module CLI (runCLI) where
 
 import AST
+import qualified Canonizer as C
 import Condition (parseConditionThrows)
 import Control.Exception (Exception (displayException), SomeException, handle, throw, throwIO)
 import Control.Exception.Base
@@ -130,6 +131,7 @@
     nonumber :: Bool,
     inPlace :: Bool,
     sequence :: Bool,
+    canonize :: Bool,
     maxDepth :: Integer,
     maxCycles :: Integer,
     rules :: [FilePath],
@@ -344,6 +346,7 @@
             <*> optNonumber
             <*> switch (long "in-place" <> help "Edit file in-place instead of printing to output")
             <*> optSequence
+            <*> switch (long "canonize" <> help "Rename all functions attached to λ binding with F1, F2, etc.")
             <*> optMaxDepth
             <*> optMaxCycles
             <*> optRule
@@ -435,7 +438,9 @@
       let listing = if null rules' then const input else (\prog -> P.printProgram' prog (sugarType, UNICODE, flat))
           xmirCtx = XmirContext omitListing omitComments listing
           printCtx = PrintProgCtx sugarType flat xmirCtx nonumber expression label outputFormat
-      rewrittens <- rewrite' program rules' (context printCtx) <&> (`H.hide` exclude)
+          canonize' = if canonize then C.canonize else id
+          hide' = (`H.hide` exclude)
+      rewrittens <- rewrite' program rules' (context printCtx) <&> hide' . canonize'
       let rewrittens' = if sequence then rewrittens else [last rewrittens]
       logDebug (printf "Printing rewritten 𝜑-program as %s" (show outputFormat))
       progs <- printRewrittens printCtx rewrittens'
@@ -445,10 +450,10 @@
         validateOpts = do
           when
             (inPlace && isNothing inputFile)
-            (invalidCLIArguments "--in-place requires an input file")
+            (invalidCLIArguments "The option --in-place requires an input file")
           when
             (inPlace && isJust targetFile)
-            (invalidCLIArguments "--in-place and --target cannot be used together")
+            (invalidCLIArguments "The options --in-place and --target cannot be used together")
           validateLatexOptions outputFormat nonumber expression label
           validateMust' must
           validateXmirOptions outputFormat omitListing omitComments
diff --git a/src/Canonizer.hs b/src/Canonizer.hs
new file mode 100644
--- /dev/null
+++ b/src/Canonizer.hs
@@ -0,0 +1,37 @@
+-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+-- SPDX-License-Identifier: MIT
+
+module Canonizer (canonize) where
+
+import AST
+import Rewriter (Rewritten)
+
+canonizeBindings :: [Binding] -> Int -> ([Binding], Int)
+canonizeBindings [] idx = ([], idx)
+canonizeBindings ((BiLambda _) : rest) idx =
+  let (bds', idx') = canonizeBindings rest (idx + 1)
+   in (BiLambda ('F' : show idx) : bds', idx')
+canonizeBindings (BiTau attr expr : rest) idx =
+  let (expr', idx') = canonizeExpression expr idx
+      (bds', idx'') = canonizeBindings rest idx'
+   in (BiTau attr expr' : bds', idx'')
+canonizeBindings (bd : rest) idx =
+  let (bds', idx') = canonizeBindings rest idx
+   in (bd : bds', idx')
+
+canonizeExpression :: Expression -> Int -> (Expression, Int)
+canonizeExpression (ExFormation bds) idx =
+  let (bds', idx') = canonizeBindings bds idx
+   in (ExFormation bds', idx')
+canonizeExpression (ExDispatch expr attr) idx =
+  let (expr', idx') = canonizeExpression expr idx
+   in (ExDispatch expr' attr, idx')
+canonizeExpression (ExApplication expr (BiTau attr arg)) idx =
+  let (expr', idx') = canonizeExpression expr idx
+      (arg', idx'') = canonizeExpression arg idx'
+   in (ExApplication expr' (BiTau attr arg'), idx'')
+canonizeExpression expr idx = (expr, idx)
+
+canonize :: [Rewritten] -> [Rewritten]
+canonize [] = []
+canonize ((Program expr, maybeRule) : rest) = (Program (fst (canonizeExpression expr 1)), maybeRule) : canonize rest
diff --git a/test/CLISpec.hs b/test/CLISpec.hs
--- a/test/CLISpec.hs
+++ b/test/CLISpec.hs
@@ -531,6 +531,12 @@
               ]
           ]
 
+    it "canonizes program" $
+      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 ⟧}"]
+
   describe "dataize" $ do
     it "dataizes simple program" $
       withStdin "Q -> [[ D> 01- ]]" $