diff --git a/Proof/Propositional/TH.hs b/Proof/Propositional/TH.hs
--- a/Proof/Propositional/TH.hs
+++ b/Proof/Propositional/TH.hs
@@ -120,7 +120,9 @@
   buildClause
     ''Empty (const $ newName "_x")
     (const $ (DVarE 'eliminate `DAppE`) . DVarE) (const asum)
-#if MIN_VERSION_th_desugar(1,10,0)
+#if MIN_VERSION_th_desugar(1,13,0)
+    (\cName ps -> [DConP cName [] $ map DVarP ps])
+#elif MIN_VERSION_th_desugar(1,10,0)
     (\cName ps -> [DConP cName $ map DVarP ps])
 #else
     (\cName ps -> [DConPa cName $ map DVarPa ps])
diff --git a/equational-reasoning.cabal b/equational-reasoning.cabal
--- a/equational-reasoning.cabal
+++ b/equational-reasoning.cabal
@@ -2,7 +2,7 @@
 --  documentation, see http://haskell.org/cabal/users-guide/
 
 name:                equational-reasoning
-version:             0.7.0.0
+version:             0.7.0.1
 synopsis:            Proof assistant for Haskell using DataKinds & PolyKinds
 description:         A simple convenient library to write equational / preorder proof as in Agda.
                      Since 0.6.0.0, this no longer depends on @singletons@ package, and the @Proof.Induction@ module goes to @equational-reasoning-induction@ package.
@@ -19,7 +19,7 @@
                       GHC == 8.6.3,
                       GHC == 8.8.2,
                       GHC == 8.10.3,
-                      GHC == 9.0.0.20201227
+                      GHC == 9.0.1
 cabal-version:       >=1.10
 source-repository head
     type: git
@@ -33,10 +33,10 @@
   ghc-options:         -Wall
   build-depends:       base             >= 4      && < 5
                      , containers       >= 0.5    && < 0.7
-                     , template-haskell >= 2.11   && < 2.17
+                     , template-haskell >= 2.11   && < 2.19
                      , void             >= 0.6    && < 0.8
   if impl(ghc >= 8.4)
-     build-depends:    th-desugar       >= 1.8 && < 1.12
+     build-depends:    th-desugar       >= 1.8 && < 1.14
   else
      build-depends:    semigroups       == 0.18.*
      build-depends:    th-desugar       >= 1.6 && < 1.8