diff --git a/equational-reasoning.cabal b/equational-reasoning.cabal
--- a/equational-reasoning.cabal
+++ b/equational-reasoning.cabal
@@ -1,43 +1,44 @@
--- Initial equational-reasoning.cabal generated by cabal init.  For further
---  documentation, see http://haskell.org/cabal/users-guide/
+name:          equational-reasoning
+version:       0.7.0.2
+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.
 
-name:                equational-reasoning
-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.
-license:             BSD3
-license-file:        LICENSE
-author:              Hiromi ISHII
-maintainer:          konn.jinro_at_gmail.com
-copyright:           (c) Hiromi ISHII 2013-2020
-category:            Math
-build-type:          Simple
-tested-with:          GHC == 8.0.2,
-                      GHC == 8.2.1,
-                      GHC == 8.4.1,
-                      GHC == 8.6.3,
-                      GHC == 8.8.2,
-                      GHC == 8.10.3,
-                      GHC == 9.0.1
-cabal-version:       >=1.10
+license:       BSD3
+license-file:  LICENSE
+author:        Hiromi ISHII
+maintainer:    konn.jinro_at_gmail.com
+copyright:     (c) Hiromi ISHII 2013-2020
+category:      Math
+build-type:    Simple
+tested-with:
+  GHC ==9.0.2
+   || ==9.2.8
+   || ==9.4.8
+   || ==9.6.3
+   || ==9.8.1
+
+cabal-version: >=1.10
+
 source-repository head
-    type: git
-    location: git://github.com/konn/equational-reasoning-in-haskell.git
+  type:     git
+  location: git://github.com/konn/equational-reasoning-in-haskell.git
 
 library
-  exposed-modules:     Proof.Equational, Proof.Propositional
-                     , Proof.Propositional.Inhabited
-                     , Proof.Propositional.Empty
-  other-modules:       Proof.Propositional.TH
-  ghc-options:         -Wall
-  build-depends:       base             >= 4      && < 5
-                     , containers       >= 0.5    && < 0.7
-                     , template-haskell >= 2.11   && < 2.19
-                     , void             >= 0.6    && < 0.8
-  if impl(ghc >= 8.4)
-     build-depends:    th-desugar       >= 1.8 && < 1.14
-  else
-     build-depends:    semigroups       == 0.18.*
-     build-depends:    th-desugar       >= 1.6 && < 1.8
-  default-language:    Haskell2010
+  exposed-modules:
+    Proof.Equational
+    Proof.Propositional
+    Proof.Propositional.Empty
+    Proof.Propositional.Inhabited
+
+  other-modules:    Proof.Propositional.TH
+  ghc-options:      -Wall
+  build-depends:
+      base              >=4    && <5
+    , containers        >=0.5  && <0.7
+    , template-haskell  >=2.11 && <2.22
+    , void              >=0.6  && <0.8
+    , th-desugar >=1.8 && <1.17
+
+  default-language: Haskell2010