diff --git a/liquidhaskell-boot.cabal b/liquidhaskell-boot.cabal
--- a/liquidhaskell-boot.cabal
+++ b/liquidhaskell-boot.cabal
@@ -1,6 +1,6 @@
 cabal-version:      2.4
 name:               liquidhaskell-boot
-version:            0.9.2.5.0
+version:            0.9.2.8.0
 synopsis:           Liquid Types for Haskell
 description:        This package provides a plugin to verify Haskell programs.
                     But most likely you should be using the [liquidhaskell package](https://hackage.haskell.org/package/liquidhaskell)
@@ -13,7 +13,7 @@
 category:           Language
 homepage:           https://github.com/ucsd-progsys/liquidhaskell
 build-type:         Simple
-tested-with:        GHC == 9.2.5
+tested-with:        GHC == 9.2.8
 
 data-files:         include/CoreToLogic.lg
                     syntax/liquid.css
diff --git a/src/Language/Haskell/Liquid/Transforms/ANF.hs b/src/Language/Haskell/Liquid/Transforms/ANF.hs
--- a/src/Language/Haskell/Liquid/Transforms/ANF.hs
+++ b/src/Language/Haskell/Liquid/Transforms/ANF.hs
@@ -249,7 +249,21 @@
        e'    <- normalize γ e
        bs    <- st_binds <$> get
        put bs'
-       return $ mkCoreLets bs e'
+       -- See Note [Shape of normalized terms]
+       let (tvs, e'') = collectTyBinders e'
+       return $ mkLams tvs (mkCoreLets bs e'')
+
+-- Note [Shape of normalized terms]
+--
+-- The termination checker in Termination.collectArguments expects the type
+-- binders to come before lets:
+--
+-- > \ (@a) -> let ... in \ b c d -> ...
+--
+-- Therefore, stitch makes sure to insert new lets after the type binders
+--
+-- > \ (@a) -> let lqanf... = ... in let ... in \ b c d -> ...
+--
 
 _mkCoreLets' :: [CoreBind] -> CoreExpr -> CoreExpr
 _mkCoreLets' bs e = mkCoreLets bs1 e1
diff --git a/src/Language/Haskell/Liquid/Types/Equality.hs b/src/Language/Haskell/Liquid/Types/Equality.hs
--- a/src/Language/Haskell/Liquid/Types/Equality.hs
+++ b/src/Language/Haskell/Liquid/Types/Equality.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE FlexibleInstances    #-}
 
--- Syntactic Equality of Types up tp forall type renaming
+-- Syntactic Equality of Types up to forall type renaming
 
 module Language.Haskell.Liquid.Types.Equality where