diff --git a/Changelog.md b/Changelog.md
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,6 +1,11 @@
 Changelog
 ==========
 
+## 0.7.1.0
+
+- Supports GHC 9.10 and 9.12
+- Drops support for GHC <9.2
+
 ## 0.7.0.2
 
 - Supports GHC 9.8
diff --git a/Proof/Equational.hs b/Proof/Equational.hs
--- a/Proof/Equational.hs
+++ b/Proof/Equational.hs
@@ -15,53 +15,52 @@
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
 {-# LANGUAGE ConstrainedClassMethods, TypeFamilyDependencies #-}
 #endif
-module Proof.Equational
-  ( (:~:) (..),
-    (:=:),
-    sym,
-    trans,
-    Equality (..),
-    Preorder (..),
-    reflexivity',
-    (:\/:),
-    (:/\:),
-    (=<=),
-    (=>=),
-    (=~=),
-    Leibniz (..),
-    Reason (..),
-    because,
-    by,
-    (===),
-    start,
-    byDefinition,
-    admitted,
-    Proxy (..),
-    cong,
-    cong',
-    Proposition (..),
-    HVec (..),
-    FromBool (..),
-    applyNAry,
-    applyNAry',
-    fromBool',
+module Proof.Equational (
+  (:~:) (..),
+  (:=:),
+  sym,
+  trans,
+  Equality (..),
+  Preorder (..),
+  reflexivity',
+  (:\/:),
+  (:/\:),
+  (=<=),
+  (=>=),
+  (=~=),
+  Leibniz (..),
+  Reason (..),
+  because,
+  by,
+  (===),
+  start,
+  byDefinition,
+  admitted,
+  Proxy (..),
+  cong,
+  cong',
+  Proposition (..),
+  HVec (..),
+  FromBool (..),
+  applyNAry,
+  applyNAry',
+  fromBool',
 
-    -- * Conversion between equalities
-    fromRefl,
-    fromLeibniz,
-    reflToLeibniz,
-    leibnizToRefl,
+  -- * Conversion between equalities
+  fromRefl,
+  fromLeibniz,
+  reflToLeibniz,
+  leibnizToRefl,
 
-    -- * Coercion
-    coerce,
-    coerceInner,
-    coerce',
-    withRefl,
+  -- * Coercion
+  coerce,
+  coerceInner,
+  coerce',
+  withRefl,
 
-    -- * Re-exported modules
-    module Data.Proxy,
-  )
-where
+  -- * Re-exported modules
+  module Data.Proxy,
+) where
 
 import Data.Kind (Type)
 import Data.Proxy
@@ -98,7 +97,7 @@
   reflexivity :: proxy a -> eq a a
   transitivity :: eq a b -> eq b c -> eq a c
 
-class Preorder eq => Equality (eq :: k -> k -> Type) where
+class (Preorder eq) => Equality (eq :: k -> k -> Type) where
   symmetry :: eq a b -> eq b a
 
 instance Preorder (:=:) where
@@ -146,22 +145,22 @@
 
 infix 5 `because`
 
-(=<=) :: Preorder r => r x y -> Reason r y z -> r x z
+(=<=) :: (Preorder r) => r x y -> Reason r y z -> r x z
 eq =<= (_ `Because` eq') = transitivity eq eq'
 {-# SPECIALIZE INLINE [1] (=<=) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}
 
-(=>=) :: Preorder r => r y z -> Reason r x y -> r x z
+(=>=) :: (Preorder r) => r y z -> Reason r x y -> r x z
 eq =>= (_ `Because` eq') = transitivity eq' eq
 {-# SPECIALIZE INLINE [1] (=>=) :: y :~: z -> Reason (:~:) x y -> x :~: z #-}
 
-(===) :: Equality eq => eq x y -> Reason eq y z -> eq x z
+(===) :: (Equality eq) => eq x y -> Reason eq y z -> eq x z
 (===) = (=<=)
 {-# SPECIALIZE INLINE [1] (===) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}
 
 (=~=) :: r x y -> proxy y -> r x y
 eq =~= _ = eq
 
-start :: Preorder eq => proxy a -> eq a a
+start :: (Preorder eq) => proxy a -> eq a a
 start = reflexivity
 
 byDefinition :: (Preorder eq) => eq a a
@@ -207,7 +206,7 @@
    It has the same effect as @'Data.Type.Equality.gcastWith'@,
    but some hacks is done to reduce runtime overhead.
 -}
-withRefl :: forall a b r. a :~: b -> (a ~ b => r) -> r
+withRefl :: forall a b r. a :~: b -> ((a ~ b) => r) -> r
 withRefl _ = gcastWith (unsafeCoerce (Refl :: () :~: ()) :: a :~: b)
 
 class Proposition (f :: k -> Type) where
@@ -239,12 +238,12 @@
 instance KnownTypeList '[] where
   viewHVec' = HNilView
 
-instance KnownTypeList ts => KnownTypeList (t ': ts) where
+instance (KnownTypeList ts) => KnownTypeList (t ': ts) where
   viewHVec' = HConsView Proxy viewHVec'
 
-newtype Magic (xs :: [Type]) a = Magic {_viewHVec' :: KnownTypeList xs => a}
+newtype Magic (xs :: [Type]) a = Magic {_viewHVec' :: (KnownTypeList xs) => a}
 
-withKnownTypeList :: forall a xs. HVecView xs -> (KnownTypeList xs => a) -> a
+withKnownTypeList :: forall a xs. HVecView xs -> ((KnownTypeList xs) => a) -> a
 withKnownTypeList xs f = (unsafeCoerce (Magic f :: Magic xs a) :: HVecView xs -> a) xs
 
 apply' :: HVecView ts -> (HVec ts -> c) -> ts :~> c
@@ -253,16 +252,16 @@
   withKnownTypeList ts $
     apply' ts (\ts' -> f $ a :- ts')
 
-applyNAry :: forall ts c. KnownTypeList ts => (HVec ts -> c) -> ts :~> c
+applyNAry :: forall ts c. (KnownTypeList ts) => (HVec ts -> c) -> ts :~> c
 applyNAry = apply' (viewHVec' :: HVecView ts)
 
-applyNAry' :: KnownTypeList ts => proxy ts -> proxy' c -> (HVec ts -> c) -> ts :~> c
+applyNAry' :: (KnownTypeList ts) => proxy ts -> proxy' c -> (HVec ts -> c) -> ts :~> c
 applyNAry' _ _ = applyNAry
 
 class FromBool (c :: Type) where
   type Predicate c :: Bool
   type Args c :: [Type]
-  fromBool :: Predicate c ~ 'True => HVec (Args c) -> c
+  fromBool :: (Predicate c ~ 'True) => HVec (Args c) -> c
 
 fromBool' :: forall proxy c. (KnownTypeList (Args c), FromBool c, Predicate c ~ 'True) => proxy c -> Args c :~> c
 fromBool' pxyc = applyNAry' (Proxy :: Proxy (Args c)) pxyc fromBool
diff --git a/Proof/Propositional.hs b/Proof/Propositional.hs
--- a/Proof/Propositional.hs
+++ b/Proof/Propositional.hs
@@ -16,32 +16,31 @@
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 
 -- | Provides type synonyms for logical connectives.
-module Proof.Propositional
-  ( type (/\),
-    type (\/),
-    Not,
-    exfalso,
-    orIntroL,
-    orIntroR,
-    orElim,
-    andIntro,
-    andElimL,
-    andElimR,
-    orAssocL,
-    orAssocR,
-    andAssocL,
-    andAssocR,
-    IsTrue (..),
-    withWitness,
-    Empty (..),
-    withEmpty,
-    withEmpty',
-    refute,
-    Inhabited (..),
-    withInhabited,
-    prove,
-  )
-where
+module Proof.Propositional (
+  type (/\),
+  type (\/),
+  Not,
+  exfalso,
+  orIntroL,
+  orIntroR,
+  orElim,
+  andIntro,
+  andElimL,
+  andElimR,
+  orAssocL,
+  orAssocR,
+  andAssocL,
+  andAssocR,
+  IsTrue (..),
+  withWitness,
+  Empty (..),
+  withEmpty,
+  withEmpty',
+  refute,
+  Inhabited (..),
+  withInhabited,
+  prove,
+) where
 
 import Data.Data (Data)
 import Data.Type.Equality (gcastWith, (:~:) (..))
@@ -105,7 +104,7 @@
 data IsTrue (b :: Bool) where
   Witness :: IsTrue 'True
 
-withWitness :: forall b r. IsTrue b -> (b ~ 'True => r) -> r
+withWitness :: forall b r. IsTrue b -> ((b ~ 'True) => r) -> r
 withWitness _ = gcastWith (unsafeCoerce (Refl :: () :~: ()) :: b :~: 'True)
 {-# NOINLINE withWitness #-}
 
@@ -126,14 +125,14 @@
 
 refute [t|0 :~: 1|]
 refute [t|() :~: Int|]
-refute [t| 'True :~: 'False|]
-refute [t| 'False :~: 'True|]
-refute [t| 'LT :~: 'GT|]
-refute [t| 'LT :~: 'EQ|]
-refute [t| 'EQ :~: 'LT|]
-refute [t| 'EQ :~: 'GT|]
-refute [t| 'GT :~: 'LT|]
-refute [t| 'GT :~: 'EQ|]
+refute [t|'True :~: 'False|]
+refute [t|'False :~: 'True|]
+refute [t|'LT :~: 'GT|]
+refute [t|'LT :~: 'EQ|]
+refute [t|'EQ :~: 'LT|]
+refute [t|'EQ :~: 'GT|]
+refute [t|'GT :~: 'LT|]
+refute [t|'GT :~: 'EQ|]
 
 prove [t|Bool|]
 prove [t|Int|]
@@ -150,4 +149,4 @@
 prove [t|IsTrue 'True|]
 
 instance Empty (IsTrue 'False) where
-  eliminate = \case
+  eliminate = \case {}
diff --git a/Proof/Propositional/Empty.hs b/Proof/Propositional/Empty.hs
--- a/Proof/Propositional/Empty.hs
+++ b/Proof/Propositional/Empty.hs
@@ -1,59 +1,75 @@
-{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
-{-# LANGUAGE DataKinds, DefaultSignatures, DeriveAnyClass, EmptyCase #-}
-{-# LANGUAGE ExplicitNamespaces, FlexibleContexts, FlexibleInstances #-}
-{-# LANGUAGE GADTs, KindSignatures, LambdaCase, PolyKinds            #-}
-{-# LANGUAGE StandaloneDeriving, TupleSections, TypeOperators        #-}
-module Proof.Propositional.Empty (Empty(..), withEmpty, withEmpty') where
-import Data.Void          (Void, absurd)
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Proof.Propositional.Empty (Empty (..), withEmpty, withEmpty') where
+
+import Data.Void (Void, absurd)
 import GHC.Generics
-import Unsafe.Coerce      (unsafeCoerce)
+import Unsafe.Coerce (unsafeCoerce)
 
--- | Type-class for types without inhabitants, dual to @'Proof.Propositional.Inhabited'@.
---   Current GHC doesn't provide selective-instance,
---   hence we don't @'Empty'@ provide instances
---   for product types in a generic deriving (DeriveAnyClass).
--- 
---   To derive an instance for each concrete types,
---   use @'Proof.Propositional.refute'@.
---
---   Since 0.4.0.0.
+{- | Type-class for types without inhabitants, dual to @'Proof.Propositional.Inhabited'@.
+  Current GHC doesn't provide selective-instance,
+  hence we don't @'Empty'@ provide instances
+  for product types in a generic deriving (DeriveAnyClass).
+
+  To derive an instance for each concrete types,
+  use @'Proof.Propositional.refute'@.
+
+  Since 0.4.0.0.
+-}
 class Empty a where
   eliminate :: a -> x
-
   default eliminate :: (Generic a, GEmpty (Rep a)) => a -> x
   eliminate = geliminate . from
 
 class GEmpty f where
   geliminate :: f a -> x
 
-instance GEmpty f => GEmpty (M1 i t f) where
+instance (GEmpty f) => GEmpty (M1 i t f) where
   geliminate (M1 a) = geliminate a
 
 instance (GEmpty f, GEmpty g) => GEmpty (f :+: g) where
   geliminate (L1 a) = geliminate a
   geliminate (R1 b) = geliminate b
 
-instance Empty c => GEmpty (K1 i c) where
+instance (Empty c) => GEmpty (K1 i c) where
   geliminate (K1 a) = eliminate a
 
 instance GEmpty V1 where
-  geliminate = \ case {}
+  geliminate = \case {}
 
 deriving instance (Empty a, Empty b) => Empty (Either a b)
+
 deriving instance Empty Void
 
-newtype MagicEmpty e a = MagicEmpty (Empty e => a)
+newtype MagicEmpty e a = MagicEmpty ((Empty e) => a)
 
--- | Giving falsity witness by proving @'Void'@ from @a@.
---   See also 'withEmpty''.
---
---   Since 0.4.0.0
-withEmpty :: forall a b. (a -> Void) -> (Empty a => b) -> b
+{- | Giving falsity witness by proving @'Void'@ from @a@.
+  See also 'withEmpty''.
+
+  Since 0.4.0.0
+-}
+withEmpty :: forall a b. (a -> Void) -> ((Empty a) => b) -> b
 withEmpty neg k = unsafeCoerce (MagicEmpty k :: MagicEmpty a b) (absurd . neg)
 
--- | Giving falsity witness by showing @a@ entails everything.
---   See also 'withEmpty'.
---
---   Since 0.4.0.0
-withEmpty' :: forall a b. (forall c. a -> c) -> (Empty a => b) -> b
+{- | Giving falsity witness by showing @a@ entails everything.
+  See also 'withEmpty'.
+
+  Since 0.4.0.0
+-}
+withEmpty' :: forall a b. (forall c. a -> c) -> ((Empty a) => b) -> b
 withEmpty' neg k = unsafeCoerce (MagicEmpty k :: MagicEmpty a b) neg
diff --git a/Proof/Propositional/Inhabited.hs b/Proof/Propositional/Inhabited.hs
--- a/Proof/Propositional/Inhabited.hs
+++ b/Proof/Propositional/Inhabited.hs
@@ -1,21 +1,35 @@
-{-# LANGUAGE DataKinds, DefaultSignatures, DeriveAnyClass, EmptyCase  #-}
-{-# LANGUAGE ExplicitNamespaces, FlexibleContexts, FlexibleInstances  #-}
-{-# LANGUAGE GADTs, KindSignatures, LambdaCase, PolyKinds, RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TupleSections   #-}
-{-# LANGUAGE TypeOperators                                            #-}
-module Proof.Propositional.Inhabited (Inhabited(..), withInhabited) where
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Proof.Propositional.Inhabited (Inhabited (..), withInhabited) where
+
 import GHC.Generics
 import Unsafe.Coerce (unsafeCoerce)
 
--- | Types with at least one inhabitant, dual to @'Proof.Propositional.Empty'@.
---   Currently, GHC doesn't provide a selective-instance,
---   hence we can't generically derive @'Inhabited'@ instances
---   for sum types (i.e. by @DeriveAnyClass@).
---
---   To derive an instance for each concrete types,
---   use @'Proof.Propositional.prove'@.
---
---   Since 0.4.0.0.
+{- | Types with at least one inhabitant, dual to @'Proof.Propositional.Empty'@.
+  Currently, GHC doesn't provide a selective-instance,
+  hence we can't generically derive @'Inhabited'@ instances
+  for sum types (i.e. by @DeriveAnyClass@).
+
+  To derive an instance for each concrete types,
+  use @'Proof.Propositional.prove'@.
+
+  Since 0.4.0.0.
+-}
 class Inhabited a where
   -- | A /generic/ inhabitant of type @'a'@, which means that
   --   one cannot assume anything about the value of @'trivial'@
@@ -24,34 +38,36 @@
   --   * is of type @a@, and
   --   * doesn't contain any partial values.
   trivial :: a
-
   default trivial :: (Generic a, GInhabited (Rep a)) => a
   trivial = to gtrivial
 
 class GInhabited f where
   gtrivial :: f a
 
-instance GInhabited f => GInhabited (M1 i t f) where
+instance (GInhabited f) => GInhabited (M1 i t f) where
   gtrivial = M1 gtrivial
 
 instance (GInhabited f, GInhabited g) => GInhabited (f :*: g) where
   gtrivial = gtrivial :*: gtrivial
 
-instance Inhabited c => GInhabited (K1 i c) where
+instance (Inhabited c) => GInhabited (K1 i c) where
   gtrivial = K1 trivial
 
 instance GInhabited U1 where
   gtrivial = U1
 
 deriving instance Inhabited ()
+
 deriving instance (Inhabited a, Inhabited b) => Inhabited (a, b)
+
 deriving instance (Inhabited a, Inhabited b, Inhabited c) => Inhabited (a, b, c)
+
 deriving instance (Inhabited a, Inhabited b, Inhabited c, Inhabited d) => Inhabited (a, b, c, d)
 
-instance Inhabited b => Inhabited (a -> b) where
+instance (Inhabited b) => Inhabited (a -> b) where
   trivial = const trivial
 
-newtype MagicInhabited a b = MagicInhabited (Inhabited a => b)
+newtype MagicInhabited a b = MagicInhabited ((Inhabited a) => b)
 
-withInhabited :: forall a b. a -> (Inhabited a => b) -> b
+withInhabited :: forall a b. a -> ((Inhabited a) => b) -> b
 withInhabited wit k = unsafeCoerce (MagicInhabited k :: MagicInhabited a b) wit
diff --git a/Proof/Propositional/TH.hs b/Proof/Propositional/TH.hs
--- a/Proof/Propositional/TH.hs
+++ b/Proof/Propositional/TH.hs
@@ -1,160 +1,182 @@
-{-# LANGUAGE CPP, ExplicitNamespaces, MultiWayIf, PatternGuards #-}
-{-# LANGUAGE TemplateHaskell, TupleSections, ViewPatterns                     #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE ViewPatterns #-}
+
 module Proof.Propositional.TH where
+
+import Control.Arrow (Kleisli (..), second)
+import Control.Monad (forM, zipWithM)
+import Data.Foldable (asum)
+import Data.Functor (void)
+import Data.Map (Map)
+import qualified Data.Map as M
+import Data.Maybe (fromJust)
+import Data.Type.Equality ((:~:) (..))
+import Language.Haskell.TH (
+  DecsQ,
+  Lit (CharL, IntegerL),
+  Name,
+  Q,
+  TypeQ,
+  isInstance,
+  newName,
+  ppr,
+ )
+import Language.Haskell.TH.Desugar (DClause (..), DCon (..), DConFields (..), DCxt, DDec (..), DExp (..), DForallTelescope (..), DInfo (..), DLetDec (DFunD), DPat (DConP, DVarP), DPred, DTyVarBndr (..), DType (..), Overlap (Overlapping), desugar, dsReify, expandType, substTy, sweeten)
 import Proof.Propositional.Empty
 import Proof.Propositional.Inhabited
 
-import           Control.Arrow               (Kleisli (..), second)
-import           Control.Monad               (forM, zipWithM)
-import           Data.Foldable               (asum)
-import           Data.Map                    (Map)
-import qualified Data.Map                    as M
-import           Data.Maybe                  (fromJust)
-import           Data.Type.Equality          ((:~:) (..))
-import           Language.Haskell.TH         (DecsQ, Lit (CharL, IntegerL),
-                                              Name, Q, TypeQ, isInstance,
-                                              newName, ppr)
-import           Language.Haskell.TH.Desugar (DClause (..), DCon (..),
-                                              DConFields (..), DCxt, DDec (..),
-                                              DExp (..), DInfo (..),
-                                              DLetDec (DFunD),
-#if MIN_VERSION_th_desugar(1,10,0)
-                                              DPat (DConP, DVarP), DPred,
+#if MIN_VERSION_th_desugar(1,18,0)
+import Language.Haskell.TH.Desugar (dLamE, dCaseE)
 #else
-                                              DPat (DConPa, DVarPa), DPred(..),
-#endif
-#if MIN_VERSION_th_desugar(1,12,0)
-  DForallTelescope(..),
-#endif
-
-                                              DTyVarBndr (..), DType (..),
-                                              Overlap (Overlapping), desugar,
-                                              dsReify, expandType, substTy,
-                                              sweeten)
-#if !MIN_VERSION_base(4,13,0)
-import           Data.Semigroup              (Semigroup (..))
-#endif
-#if MIN_VERSION_th_desugar(1,12,0)
-import Data.Functor (void)
+import Language.Haskell.TH.Desugar (DMatch)
 #endif
 
+mkDInstanceD ::
+  Maybe Overlap ->
+  DCxt ->
+  DType ->
+  [DDec] ->
+  DDec
+mkDInstanceD ovl ctx dtype ddecs = DInstanceD ovl Nothing ctx dtype ddecs
 
--- | Macro to automatically derive @'Empty'@ instance for
---   concrete (variable-free) types which may contain products.
+{- | Macro to automatically derive @'Empty'@ instance for
+  concrete (variable-free) types which may contain products.
+-}
 refute :: TypeQ -> DecsQ
 refute tps = do
   tp <- expandType =<< desugar =<< tps
   let Just (_, tyName, args) = splitType tp
-      mkInst dxt cls = return $ sweeten
-                       [DInstanceD (Just Overlapping)
-#if MIN_VERSION_th_desugar(1,10,0)
-                        Nothing
-#endif
-                        dxt
-                        (DAppT (DConT ''Empty) (foldl DAppT (DConT tyName) args))
-                        [DLetDec $ DFunD 'eliminate cls]
-                         ]
+      mkInst dxt cls =
+        return $
+          sweeten
+            [ mkDInstanceD
+                (Just Overlapping)
+                dxt
+                (DAppT (DConT ''Empty) (foldl DAppT (DConT tyName) args))
+                [DLetDec $ DFunD 'eliminate cls]
+            ]
   if tyName == ''(:~:)
     then do
       let [l, r] = args
-      v    <- newName "_v"
+      v <- newName "_v"
       dist <- compareType l r
       case dist of
-        NonEqual    -> mkInst [] [DClause [] $ DLamE [v] (DCaseE (DVarE v) []) ]
-        Equal       -> fail $ "Equal: " ++ show (ppr $ sweeten l) ++ " ~ " ++ show (ppr $ sweeten r)
-        Undecidable -> fail $ "No enough info to check non-equality: " ++
-                         show (ppr $ sweeten l) ++ " ~ " ++ show (ppr $ sweeten r)
+        NonEqual -> mkInst [] [DClause [] $ dLamE' [v] (dCaseE (DVarE v) [])]
+        Equal -> fail $ "Equal: " ++ show (ppr $ sweeten l) ++ " ~ " ++ show (ppr $ sweeten r)
+        Undecidable ->
+          fail $
+            "No enough info to check non-equality: "
+              ++ show (ppr $ sweeten l)
+              ++ " ~ "
+              ++ show (ppr $ sweeten r)
     else do
       (dxt, cons) <- resolveSubsts args . fromJust =<< dsReify tyName
       Just cls <- sequence <$> mapM buildRefuteClause cons
       mkInst dxt cls
 
--- | Macro to automatically derive @'Inhabited'@ instance for
---   concrete (variable-free) types which may contain sums.
+#if !MIN_VERSION_th_desugar(1,18,0)
+dCaseE :: DExp -> [DMatch] -> DExp
+dCaseE = DCaseE
+#endif
+
+dLamE' :: [Name] -> DExp -> DExp
+#if MIN_VERSION_th_desugar(1,18,0)
+dLamE' = dLamE . map DVarP
+#else
+dLamE' = DLamE
+#endif
+
+{- | Macro to automatically derive @'Inhabited'@ instance for
+  concrete (variable-free) types which may contain sums.
+-}
 prove :: TypeQ -> DecsQ
 prove tps = do
   tp <- expandType =<< desugar =<< tps
   let Just (_, tyName, args) = splitType tp
-      mkInst dxt cls = return $ sweeten
-                       [DInstanceD (Just Overlapping)
-#if MIN_VERSION_th_desugar(1,10,0)
-                        Nothing
-#endif
-                        dxt
-                        (DAppT (DConT ''Inhabited) (foldl DAppT (DConT tyName) args))
-                        [DLetDec $ DFunD 'trivial cls]
-                         ]
+      mkInst dxt cls =
+        return $
+          sweeten
+            [ mkDInstanceD
+                (Just Overlapping)
+                dxt
+                (DAppT (DConT ''Inhabited) (foldl DAppT (DConT tyName) args))
+                [DLetDec $ DFunD 'trivial cls]
+            ]
   isNum <- isInstance ''Num [sweeten tp]
 
-  if | isNum -> mkInst [] [DClause [] $ DLitE $ IntegerL 0 ]
-     | tyName == ''Char  -> mkInst [] [DClause [] $ DLitE $ CharL '\NUL']
-     | tyName == ''(:~:) -> do
+  if
+    | isNum -> mkInst [] [DClause [] $ DLitE $ IntegerL 0]
+    | tyName == ''Char -> mkInst [] [DClause [] $ DLitE $ CharL '\NUL']
+    | tyName == ''(:~:) -> do
         let [l, r] = args
         dist <- compareType l r
         case dist of
-          NonEqual    -> fail $ "Equal: " ++ show (ppr $ sweeten l) ++ " ~ " ++ show (ppr $ sweeten r)
-          Equal       -> mkInst [] [DClause [] $ DConE 'Refl ]
-          Undecidable -> fail $ "No enough info to check non-equality: " ++
-                           show (ppr $ sweeten l) ++ " ~ " ++ show (ppr $ sweeten r)
-     | otherwise -> do
+          NonEqual -> fail $ "Equal: " ++ show (ppr $ sweeten l) ++ " ~ " ++ show (ppr $ sweeten r)
+          Equal -> mkInst [] [DClause [] $ DConE 'Refl]
+          Undecidable ->
+            fail $
+              "No enough info to check non-equality: "
+                ++ show (ppr $ sweeten l)
+                ++ " ~ "
+                ++ show (ppr $ sweeten r)
+    | otherwise -> do
         (dxt, cons) <- resolveSubsts args . fromJust =<< dsReify tyName
         Just cls <- asum <$> mapM buildProveClause cons
         mkInst dxt [cls]
 
-buildClause :: Name -> (DType -> Q b) -> (DType -> b -> DExp)
-            -> (Name -> [Maybe DExp] -> Maybe DExp) -> (Name -> [b] -> [DPat])
-            -> DCon -> Q (Maybe DClause)
+buildClause ::
+  Name ->
+  (DType -> Q b) ->
+  (DType -> b -> DExp) ->
+  (Name -> [Maybe DExp] -> Maybe DExp) ->
+  (Name -> [b] -> [DPat]) ->
+  DCon ->
+  Q (Maybe DClause)
 buildClause clsName genPlaceHolder buildFactor flattenExps toPats (DCon _ _ cName flds _) = do
   let tys = fieldsVars flds
   varDic <- mapM genPlaceHolder tys
   fmap (DClause $ toPats cName varDic) . flattenExps cName <$> zipWithM tryProc tys varDic
   where
     tryProc ty name = do
-      isEmpty <- isInstance clsName . (:[]) $ sweeten ty
-      return $ if isEmpty
-        then Just $ buildFactor ty name
-        else Nothing
+      isEmpty <- isInstance clsName . (: []) $ sweeten ty
+      return $
+        if isEmpty
+          then Just $ buildFactor ty name
+          else Nothing
 
 buildRefuteClause :: DCon -> Q (Maybe DClause)
 buildRefuteClause =
   buildClause
-    ''Empty (const $ newName "_x")
-    (const $ (DVarE 'eliminate `DAppE`) . DVarE) (const asum)
-#if MIN_VERSION_th_desugar(1,13,0)
+    ''Empty
+    (const $ newName "_x")
+    (const $ (DVarE 'eliminate `DAppE`) . DVarE)
+    (const asum)
     (\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])
-#endif
 
 buildProveClause :: DCon -> Q (Maybe DClause)
-buildProveClause  =
+buildProveClause =
   buildClause
-    ''Inhabited (const $ return ())
+    ''Inhabited
+    (const $ return ())
     (const $ const $ DVarE 'trivial)
-    (\ con args -> foldl DAppE (DConE con) <$> sequence args )
+    (\con args -> foldl DAppE (DConE con) <$> sequence args)
     (const $ const [])
 
 fieldsVars :: DConFields -> [DType]
-#if MIN_VERSION_th_desugar(1,8,0)
-fieldsVars (DNormalC _ fs)
-#else
-fieldsVars (DNormalC fs)
-#endif
-  = map snd fs
-fieldsVars (DRecC fs)    = map (\(_,_,c) -> c) fs
+fieldsVars (DNormalC _ fs) = map snd fs
+fieldsVars (DRecC fs) = map (\(_, _, c) -> c) fs
 
 resolveSubsts :: [DType] -> DInfo -> Q (DCxt, [DCon])
 resolveSubsts args info =
   case info of
-    (DTyConI (DDataD _ cxt _ tvbs
-#if MIN_VERSION_th_desugar(1,9,0)
-              _
-#endif
-             dcons _) _) -> do
+    DTyConI (DDataD _ cxt _ tvbs _ dcons _) _ -> do
       let dic = M.fromList $ zip (map dtvbToName tvbs) args
-      (cxt , ) <$> mapM (substDCon dic) dcons
+      (cxt,) <$> mapM (substDCon dic) dcons
     -- (DTyConI (DOpenTypeFamilyD n) _) ->  return []
     -- (DTyConI (DClosedTypeFamilyD _ ddec2) minst) ->  return []
     -- (DTyConI (DDataFamilyD _ ddec2) minst) ->  return []
@@ -168,63 +190,38 @@
 substDCon dic (DCon forall'd cxt conName fields mPhantom) =
   DCon forall'd cxt conName
     <$> substFields dic fields
-#if MIN_VERSION_th_desugar(1,9,0)
     <*> substTy dic mPhantom
-#else
-    <*> mapM (substTy dic) mPhantom
-#endif
 
 substFields :: SubstDic -> DConFields -> Q DConFields
-substFields subst
-#if MIN_VERSION_th_desugar(1,8,0)
-  (DNormalC fixi fs)
-#else
-  (DNormalC fs)
-#endif
-  =
-#if MIN_VERSION_th_desugar(1,8,0)
-  DNormalC fixi <$>
-#else
-  DNormalC <$>
-#endif
-  mapM (runKleisli $ second $ Kleisli $ substTy subst) fs
+substFields
+  subst
+  (DNormalC fixi fs) =
+    DNormalC fixi
+      <$> mapM (runKleisli $ second $ Kleisli $ substTy subst) fs
 substFields subst (DRecC fs) =
-  DRecC <$> forM fs (\(a,b,c) -> (a, b ,) <$> substTy subst c)
+  DRecC <$> forM fs (\(a, b, c) -> (a,b,) <$> substTy subst c)
 
 splitType :: DType -> Maybe ([Name], Name, [DType])
-#if MIN_VERSION_th_desugar(1,11,0)
 splitType (DConstrainedT _ t) = splitType t
-#if MIN_VERSION_th_desugar(1,12,0)
-splitType (DForallT (unTelescope -> vs) t) 
-#else
-splitType (DForallT _ vs t) 
-#endif
-#else
-splitType (DForallT vs _ t) 
-#endif
-  = (\(a,b,c) -> (map dtvbToName vs ++ a, b, c)) <$> splitType t
-splitType (DAppT t1 t2) = (\(a,b,c) -> (a, b, c ++ [t2])) <$> splitType t1
+splitType (DForallT (unTelescope -> vs) t) =
+  (\(a, b, c) -> (map dtvbToName vs ++ a, b, c)) <$> splitType t
+splitType (DAppT t1 t2) = (\(a, b, c) -> (a, b, c ++ [t2])) <$> splitType t1
 splitType (DSigT t _) = splitType t
 splitType (DVarT _) = Nothing
 splitType (DConT n) = Just ([], n, [])
 splitType DArrowT = Just ([], ''(->), [])
 splitType (DLitT _) = Nothing
 splitType DWildCardT = Nothing
-#if !MIN_VERSION_th_desugar(1,9,0)
-splitType DStarT = Nothing
-#elif MIN_VERSION_th_desugar(1,10,0)
 splitType (DAppKindT _ _) = Nothing
-#endif
 
-
 data EqlJudge = NonEqual | Undecidable | Equal
-              deriving (Read, Show, Eq, Ord)
+  deriving (Read, Show, Eq, Ord)
 
 instance Semigroup EqlJudge where
-  NonEqual    <> _        = NonEqual
+  NonEqual <> _ = NonEqual
   Undecidable <> NonEqual = NonEqual
-  Undecidable <> _        = Undecidable
-  Equal       <> m        = m
+  Undecidable <> _ = Undecidable
+  Equal <> m = m
 
 instance Monoid EqlJudge where
   mappend = (<>)
@@ -237,69 +234,50 @@
   compareType' t s
 
 compareType' :: DType -> DType -> Q EqlJudge
-compareType' (DSigT t1 t2) (DSigT s1 s2)
-  = (<>) <$> compareType' t1 s1 <*> compareType' t2 s2
-compareType' (DSigT t _) s
-  = compareType' t s
-compareType' t (DSigT s _)
-  = compareType' t s
+compareType' (DSigT t1 t2) (DSigT s1 s2) =
+  (<>) <$> compareType' t1 s1 <*> compareType' t2 s2
+compareType' (DSigT t _) s =
+  compareType' t s
+compareType' t (DSigT s _) =
+  compareType' t s
 compareType' (DVarT t) (DVarT s)
-  | t == s    = return Equal
+  | t == s = return Equal
   | otherwise = return Undecidable
 compareType' (DVarT _) _ = return Undecidable
 compareType' _ (DVarT _) = return Undecidable
 compareType' DWildCardT _ = return Undecidable
 compareType' _ DWildCardT = return Undecidable
-#if MIN_VERSION_th_desugar(1,11,0)
 compareType' (DConstrainedT tCxt t) (DConstrainedT sCxt s) = do
   pd <- compareCxt tCxt sCxt
   bd <- compareType' t s
   return (pd <> bd)
-compareType' DConstrainedT{} _ = return NonEqual
-#if MIN_VERSION_th_desugar(1,12,0)
+compareType' DConstrainedT {} _ = return NonEqual
 compareType' (DForallT (unTelescope -> tTvBs) t) (DForallT (unTelescope -> sTvBs) s)
-#else
-compareType' (DForallT _ tTvBs t) (DForallT _ sTvBs s)
-#endif
   | length tTvBs == length sTvBs = do
       let dic = M.fromList $ zip (map dtvbToName sTvBs) (map (DVarT . dtvbToName) tTvBs)
       s' <- substTy dic s
       bd <- compareType' t s'
       return bd
   | otherwise = return NonEqual
-#else
-compareType' (DForallT tTvBs tCxt t) (DForallT sTvBs sCxt s)
-  | length tTvBs == length sTvBs = do
-      let dic = M.fromList $ zip (map dtvbToName sTvBs) (map (DVarT . dtvbToName) tTvBs)
-      s' <- substTy dic s
-      pd <- compareCxt tCxt =<< mapM (substPred dic) sCxt
-      bd <- compareType' t s'
-      return (pd <> bd)
-  | otherwise = return NonEqual
-#endif
-compareType' DForallT{} _   = return NonEqual
-compareType' (DAppT t1 t2) (DAppT s1 s2)
-  = (<>) <$> compareType' t1 s1 <*> compareType' t2 s2
+compareType' DForallT {} _ = return NonEqual
+compareType' (DAppT t1 t2) (DAppT s1 s2) =
+  (<>) <$> compareType' t1 s1 <*> compareType' t2 s2
 compareType' (DConT t) (DConT s)
-  | t == s    = return Equal
+  | t == s = return Equal
   | otherwise = return NonEqual
 compareType' (DConT _) _ = return NonEqual
 compareType' DArrowT DArrowT = return Equal
 compareType' DArrowT _ = return NonEqual
 compareType' (DLitT t) (DLitT s)
-  | t == s    = return Equal
+  | t == s = return Equal
   | otherwise = return NonEqual
 compareType' (DLitT _) _ = return NonEqual
-#if !MIN_VERSION_th_desugar(1,9,0)
-compareType' DStarT DStarT = return NonEqual
-#endif
 compareType' _ _ = return NonEqual
 
 compareCxt :: DCxt -> DCxt -> Q EqlJudge
 compareCxt l r = mconcat <$> zipWithM comparePred l r
 
 comparePred :: DPred -> DPred -> Q EqlJudge
-#if MIN_VERSION_th_desugar(1,10,0)
 comparePred DWildCardT _ = return Undecidable
 comparePred _ DWildCardT = return Undecidable
 comparePred (DVarT l) (DVarT r)
@@ -319,71 +297,23 @@
   | l == r = return Equal
   | otherwise = return NonEqual
 comparePred (DConT _) _ = return NonEqual
-#if MIN_VERSION_th_desugar(1,12,0)
 comparePred (DForallT _ _) (DForallT _ _) = return Undecidable
-#else
-comparePred (DForallT _ _ _) (DForallT _ _ _) = return Undecidable
-#endif
-comparePred (DForallT{}) _ = return NonEqual
+comparePred (DForallT {}) _ = return NonEqual
 comparePred _ _ = fail "Kind error: Expecting type-level predicate"
-#else
-comparePred DWildCardPr _ = return Undecidable
-comparePred _ DWildCardPr = return Undecidable
-comparePred (DVarPr l) (DVarPr r)
-  | l == r = return Equal
-comparePred (DVarPr _) _ = return Undecidable
-comparePred _ (DVarPr _) = return Undecidable
-comparePred (DSigPr l t) (DSigPr r s) =
-  (<>) <$> compareType' t s <*> comparePred l r
-comparePred (DSigPr l _) r = comparePred l r
-comparePred l (DSigPr r _) = comparePred l r
-comparePred (DAppPr l1 l2) (DAppPr r1 r2) = do
-  l2' <- expandType l2
-  r2' <- expandType r2
-  (<>) <$> comparePred l1 r1 <*> compareType' l2' r2'
-comparePred (DAppPr _ _) _ = return NonEqual
-comparePred (DConPr l) (DConPr r)
-  | l == r = return Equal
-  | otherwise = return NonEqual
-comparePred (DConPr _) _ = return NonEqual
-#if MIN_VERSION_th_desugar(1,9,0)
-comparePred (DForallPr _ _ _) (DForallPr _ _ _) = return Undecidable
-comparePred (DForallPr{}) _ = return NonEqual
-#endif
-#endif
 
 substPred :: SubstDic -> DPred -> Q DPred
-#if MIN_VERSION_th_desugar(1,10,0)
 substPred dic (DAppT p1 p2) = DAppT <$> substPred dic p1 <*> (expandType =<< substTy dic p2)
-substPred dic (DSigT p knd) = DSigT <$> substPred dic p  <*> (expandType =<< substTy dic knd)
+substPred dic (DSigT p knd) = DSigT <$> substPred dic p <*> (expandType =<< substTy dic knd)
 substPred dic prd@(DVarT p)
   | Just (DVarT t) <- M.lookup p dic = return $ DVarT t
   | Just (DConT t) <- M.lookup p dic = return $ DConT t
   | otherwise = return prd
 substPred _ t = return t
-#else
-substPred dic (DAppPr p1 p2) = DAppPr <$> substPred dic p1 <*> (expandType =<< substTy dic p2)
-substPred dic (DSigPr p knd) = DSigPr <$> substPred dic p  <*> (expandType =<< substTy dic knd)
-substPred dic prd@(DVarPr p)
-  | Just (DVarT t) <- M.lookup p dic = return $ DVarPr t
-  | Just (DConT t) <- M.lookup p dic = return $ DConPr t
-  | otherwise = return prd
-substPred _ t = return t
-#endif
 
-{- FOURMOLU_DISABLE -}
-#if MIN_VERSION_th_desugar(1,12,0)
 dtvbToName :: DTyVarBndr flag -> Name
-dtvbToName (DPlainTV n _)    = n
+dtvbToName (DPlainTV n _) = n
 dtvbToName (DKindedTV n _ _) = n
-#else
-dtvbToName :: DTyVarBndr -> Name
-dtvbToName (DPlainTV n)    = n
-dtvbToName (DKindedTV n _) = n
-#endif
 
-#if MIN_VERSION_th_desugar(1,12,0)
 unTelescope :: DForallTelescope -> [DTyVarBndr ()]
 unTelescope (DForallVis vis) = map void vis
 unTelescope (DForallInvis vis) = map void vis
-#endif
diff --git a/equational-reasoning.cabal b/equational-reasoning.cabal
--- a/equational-reasoning.cabal
+++ b/equational-reasoning.cabal
@@ -1,6 +1,6 @@
 cabal-version: 3.4
 name: equational-reasoning
-version: 0.7.0.3
+version: 0.7.1.0
 synopsis: Proof assistant for Haskell using DataKinds & PolyKinds
 description:
   A simple convenient library to write equational / preorder proof as in Agda.
@@ -14,7 +14,7 @@
 category: Math
 build-type: Simple
 tested-with:
-  ghc ==9.0.2 || ==9.2.8 || ==9.4.8 || ==9.6.5 || ==9.8.2
+  ghc ==9.2.8 || ==9.4.8 || ==9.6.5 || ==9.8.4 || ==9.10.1 || ==9.12.1
 
 extra-doc-files:
   Changelog.md
@@ -25,6 +25,7 @@
   location: git://github.com/konn/equational-reasoning-in-haskell.git
 
 library
+  -- cabal-gild: discover ./Proof/**/*.hs --exclude Proof/Propositional/TH.hs
   exposed-modules:
     Proof.Equational
     Proof.Propositional
@@ -34,10 +35,10 @@
   other-modules: Proof.Propositional.TH
   ghc-options: -Wall
   build-depends:
-    base >=4 && <5,
-    containers >=0.5 && <0.7,
-    template-haskell >=2.11 && <2.23,
-    th-desugar >=1.8 && <1.18,
+    base >=4.13 && <5,
+    containers >=0.5 && <0.8,
+    template-haskell >=2.11 && <2.24,
+    th-desugar >=1.13 && <1.19,
     void >=0.6 && <0.8,
 
   default-language: Haskell2010