diff --git a/Proof/Equational.hs b/Proof/Equational.hs
--- a/Proof/Equational.hs
+++ b/Proof/Equational.hs
@@ -1,39 +1,86 @@
-{-# LANGUAGE CPP, DataKinds, FlexibleContexts, GADTs, KindSignatures #-}
-{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables              #-}
-{-# LANGUAGE StandaloneDeriving, TypeFamilies, TypeOperators         #-}
-{-# LANGUAGE TypeSynonymInstances, UndecidableInstances              #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+
 #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'
-                          -- * Conversion between equalities
-                        , fromRefl, fromLeibniz, reflToLeibniz, leibnizToRefl
-                          -- * Coercion
-                        , coerce, coerce', withRefl
-                          -- * Re-exported modules
-                        , module Data.Proxy
-                        ) where
+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,
+
+    -- * Coercion
+    coerce,
+    coerceInner,
+    coerce',
+    withRefl,
+
+    -- * Re-exported modules
+    module Data.Proxy,
+  )
+where
+
+import Data.Kind (Type)
 import Data.Proxy
 import Data.Type.Equality hiding (apply)
 import Unsafe.Coerce
 
 infix 4 :=:
+
 type a :\/: b = Either a b
+
 infixr 2 :\/:
 
 type a :/\: b = (a, b)
+
 infixr 3 :/\:
 
 type (:=:) = (:~:)
 
-data Leibniz a b = Leibniz { apply :: forall f. f a -> f b }
+data Leibniz a b = Leibniz {apply :: forall f. f a -> f b}
 
 leibnizToRefl :: Leibniz a b -> a :=: b
 leibnizToRefl eq = apply eq Refl
@@ -47,25 +94,25 @@
 reflToLeibniz :: a :=: b -> Leibniz a b
 reflToLeibniz Refl = Leibniz id
 
-class Preorder (eq :: k -> k -> *) where
-  reflexivity  :: proxy a -> eq a a
-  transitivity :: eq a b  -> eq b c -> eq a c
+class Preorder (eq :: k -> k -> Type) where
+  reflexivity :: proxy a -> eq a a
+  transitivity :: eq a b -> eq b c -> eq a c
 
-class Preorder eq => Equality (eq :: k -> k -> *) where
-  symmetry     :: eq a b  -> eq b a
+class Preorder eq => Equality (eq :: k -> k -> Type) where
+  symmetry :: eq a b -> eq b a
 
 instance Preorder (:=:) where
-  {-# SPECIALISE instance Preorder (:=:) #-}
+  {-# SPECIALIZE instance Preorder (:=:) #-}
   transitivity Refl Refl = Refl
-  {-# INLINE[1] transitivity #-}
+  {-# INLINE [1] transitivity #-}
 
-  reflexivity  _         = Refl
-  {-# INLINE[1] reflexivity #-}
+  reflexivity _ = Refl
+  {-# INLINE [1] reflexivity #-}
 
 instance Equality (:=:) where
-  {-# SPECIALISE instance Equality (:~:) #-}
-  symmetry     Refl      = Refl
-  {-# INLINE[1] symmetry #-}
+  {-# SPECIALIZE instance Equality (:~:) #-}
+  symmetry Refl = Refl
+  {-# INLINE [1] symmetry #-}
 
 instance Preorder (->) where
   reflexivity _ = id
@@ -79,9 +126,9 @@
   transitivity (Leibniz aEqb) (Leibniz bEqc) = Leibniz $ bEqc . aEqb
 
 instance Equality Leibniz where
-  symmetry eq  = unFlip $ apply eq $ Flip leibniz_refl
+  symmetry eq = unFlip $ apply eq $ Flip leibniz_refl
 
-newtype Flip f a b = Flip { unFlip :: f b a }
+newtype Flip f a b = Flip {unFlip :: f b a}
 
 data Reason eq x y where
   Because :: proxy y -> eq x y -> Reason eq x y
@@ -91,25 +138,25 @@
 
 by, because :: proxy y -> eq x y -> Reason eq x y
 because = Because
-by      = Because
+by = Because
 
 infixl 4 ===, =<=, =~=, =>=
+
 infix 5 `Because`
+
 infix 5 `because`
 
 (=<=) :: Preorder r => r x y -> Reason r y z -> r x z
 eq =<= (_ `Because` eq') = transitivity eq eq'
-
-{-# SPECIALISE INLINE[1] (=<=) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}
+{-# SPECIALIZE INLINE [1] (=<=) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}
 
 (=>=) :: Preorder r => r y z -> Reason r x y -> r x z
 eq =>= (_ `Because` eq') = transitivity eq' eq
-
-{-# SPECIALISE INLINE[1] (=>=) :: y :~: z -> Reason (:~:) x y -> x :~: z #-}
+{-# SPECIALIZE INLINE [1] (=>=) :: y :~: z -> Reason (:~:) x y -> x :~: z #-}
 
 (===) :: Equality eq => eq x y -> Reason eq y z -> eq x z
 (===) = (=<=)
-{-# SPECIALISE INLINE[1] (===) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}
+{-# SPECIALIZE INLINE [1] (===) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}
 
 (=~=) :: r x y -> proxy y -> r x y
 eq =~= _ = eq
@@ -128,63 +175,65 @@
 cong Proxy Refl = Refl
 
 cong' :: (pxy m -> pxy (f m)) -> a :=: b -> f a :=: f b
-cong' _ Refl =  Refl
+cong' _ Refl = Refl
 
--- | Type coercion. 'coerce' is using @unsafeCoerce a@.
--- So, please, please do not provide the @undefined@ as the proof.
--- Using this function instead of pattern-matching on equality proof,
--- you can reduce the overhead introduced by run-time proof.
-coerce :: (a :=: b) -> f a -> f b
-coerce _ a = unsafeCoerce a
-{-# INLINE[1] coerce #-}
+{- | Type coercion. 'coerce' is using @unsafeCoerce a@.
+ So, please, please do not provide the @undefined@ as the proof.
+ Using this function instead of pattern-matching on equality proof,
+ you can reduce the overhead introduced by run-time proof.
+-}
+coerceInner, coerce :: (a :=: b) -> f a -> f b
+{-# DEPRECATED coerce "Use coerceInner instead" #-}
+coerce = coerceInner
+{-# INLINE coerce #-}
+coerceInner _ = unsafeCoerce
+{-# INLINE [1] coerceInner #-}
 
 -- | Coercion for identity types.
 coerce' :: a :=: b -> a -> b
-coerce' _ a = unsafeCoerce a
-{-# INLINE[1] coerce' #-}
+coerce' _ = unsafeCoerce
+{-# INLINE [1] coerce' #-}
 
 {-# RULES
 "coerce/unsafeCoerce" [~1] forall xs.
-  coerce xs = unsafeCoerce
+  coerceInner xs =
+    unsafeCoerce
 "coerce'/unsafeCoerce" [~1] forall xs.
-  coerce' xs = unsafeCoerce
+  coerce' xs =
+    unsafeCoerce
   #-}
 
--- | Solves equality constraint without explicit coercion.
---   It has the same effect as @'Data.Type.Equality.gcastWith'@,
---   but some hacks is done to reduce runtime overhead.
+{- | Solves equality constraint without explicit coercion.
+   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 _ r = case unsafeCoerce (Refl :: () :~: ()) :: a :~: b of
-  Refl -> r
-{-# NOINLINE withRefl #-}
-{-# RULES
-"withRefl/unsafeCoerce" [~1] forall x.
-  withRefl x = unsafeCoerce
-  #-}
+withRefl _ = gcastWith (unsafeCoerce (Refl :: () :~: ()) :: a :~: b)
 
-class Proposition (f :: k -> *) where
-  type OriginalProp (f :: k -> *) (n :: k) :: *
+class Proposition (f :: k -> Type) where
+  type OriginalProp (f :: k -> Type) (n :: k) :: Type
   unWrap :: f n -> OriginalProp f n
-  wrap   :: OriginalProp f n -> f n
+  wrap :: OriginalProp f n -> f n
 
-data HVec (xs :: [*]) where
+data HVec (xs :: [Type]) where
   HNil :: HVec '[]
   (:-) :: x -> HVec xs -> HVec (x ': xs)
 
 infixr 9 :-
-type family (xs :: [*]) :~> (a :: *) :: * where
-  '[]       :~> a = a
+
+type family (xs :: [Type]) :~> (a :: Type) :: Type where
+  '[] :~> a = a
   (x ': xs) :~> a = x -> (xs :~> a)
 
 infixr 1 :~>
 
-data HVecView (xs :: [*]) :: * where
-  HNilView  :: HVecView '[]
+data HVecView (xs :: [Type]) :: Type where
+  HNilView :: HVecView '[]
   HConsView :: Proxy t -> HVecView ts -> HVecView (t ': ts)
 
 deriving instance Show (HVecView xs)
 
-class KnownTypeList (xs :: [*]) where
+class KnownTypeList (xs :: [Type]) where
   viewHVec' :: HVecView xs
 
 instance KnownTypeList '[] where
@@ -193,15 +242,16 @@
 instance KnownTypeList ts => KnownTypeList (t ': ts) where
   viewHVec' = HConsView Proxy viewHVec'
 
-newtype Magic (xs :: [*]) 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 xs f = (unsafeCoerce (Magic f :: Magic xs a) :: HVecView xs -> a) xs
 
 apply' :: HVecView ts -> (HVec ts -> c) -> ts :~> c
 apply' HNilView f = f HNil
-apply' (HConsView Proxy ts) f = \a -> withKnownTypeList ts $
-  apply' ts (\ts' -> f $ a :- ts')
+apply' (HConsView Proxy ts) f = \a ->
+  withKnownTypeList ts $
+    apply' ts (\ts' -> f $ a :- ts')
 
 applyNAry :: forall ts c. KnownTypeList ts => (HVec ts -> c) -> ts :~> c
 applyNAry = apply' (viewHVec' :: HVecView ts)
@@ -209,10 +259,10 @@
 applyNAry' :: KnownTypeList ts => proxy ts -> proxy' c -> (HVec ts -> c) -> ts :~> c
 applyNAry' _ _ = applyNAry
 
-class FromBool (c :: *) where
+class FromBool (c :: Type) where
   type Predicate c :: Bool
-  type Args c :: [*]
+  type Args c :: [Type]
   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' :: 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
@@ -1,34 +1,65 @@
-{-# LANGUAGE DataKinds, DeriveDataTypeable, EmptyCase, ExplicitForAll     #-}
-{-# LANGUAGE ExplicitNamespaces, FlexibleInstances, GADTs, KindSignatures #-}
-{-# LANGUAGE LambdaCase, PolyKinds, RankNTypes, StandaloneDeriving        #-}
-{-# LANGUAGE TemplateHaskell, TypeOperators                               #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeOperators #-}
 {-# 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
+  ( 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, (:~:) (..))
+import Data.Typeable (Typeable)
+import Data.Void
 import Proof.Propositional.Empty
 import Proof.Propositional.Inhabited
 import Proof.Propositional.TH
-
-import Data.Data          (Data)
-import Data.Type.Equality ((:~:))
-import Data.Typeable      (Typeable)
-import Data.Void
 import Unsafe.Coerce
 
 type a /\ b = (a, b)
+
 type a \/ b = Either a b
-type Not a  = a -> Void
 
+type Not a = a -> Void
+
 infixr 2 \/
+
 infixr 3 /\
 
 exfalso :: a -> Not a -> b
@@ -53,69 +84,70 @@
 andElimR = snd
 
 andAssocL :: a /\ (b /\ c) -> (a /\ b) /\ c
-andAssocL (a,(b,c)) = ((a,b), c)
+andAssocL (a, (b, c)) = ((a, b), c)
 
 andAssocR :: (a /\ b) /\ c -> a /\ (b /\ c)
-andAssocR ((a,b),c) = (a,(b,c))
+andAssocR ((a, b), c) = (a, (b, c))
 
 orAssocL :: a \/ (b \/ c) -> (a \/ b) \/ c
-orAssocL (Left a)          = Left (Left a)
-orAssocL (Right (Left b))  = Left (Right b)
+orAssocL (Left a) = Left (Left a)
+orAssocL (Right (Left b)) = Left (Right b)
 orAssocL (Right (Right c)) = Right c
 
 orAssocR :: (a \/ b) \/ c -> a \/ (b \/ c)
-orAssocR (Left (Left a))  = Left a
+orAssocR (Left (Left a)) = Left a
 orAssocR (Left (Right b)) = Right (Left b)
-orAssocR (Right c)        = Right (Right c)
-
+orAssocR (Right c) = Right (Right c)
 
--- | Utility type to convert type-level (@'Bool'@-valued) predicate function
---   into concrete witness data-type.
+{- | Utility type to convert type-level (@'Bool'@-valued) predicate function
+   into concrete witness data-type.
+-}
 data IsTrue (b :: Bool) where
   Witness :: IsTrue 'True
 
-withWitness :: IsTrue b -> (b ~ 'True => r) -> r
-withWitness Witness r = r
+withWitness :: forall b r. IsTrue b -> (b ~ 'True => r) -> r
+withWitness _ = gcastWith (unsafeCoerce (Refl :: () :~: ()) :: b :~: 'True)
 {-# NOINLINE withWitness #-}
-{-# RULES
-"withWitness/coercion" [~1] forall x.
-  withWitness x = unsafeCoerce
-  #-}
 
 deriving instance Show (IsTrue b)
-deriving instance Eq   (IsTrue b)
-deriving instance Ord  (IsTrue b)
+
+deriving instance Eq (IsTrue b)
+
+deriving instance Ord (IsTrue b)
+
 deriving instance Read (IsTrue 'True)
+
 deriving instance Typeable IsTrue
+
 deriving instance Data (IsTrue 'True)
 
 instance {-# OVERLAPPABLE #-} (Inhabited a, Empty b) => Empty (a -> b) where
   eliminate f = eliminate (f trivial)
 
-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|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|]
 
-prove [t| Bool |]
-prove [t| Int |]
-prove [t| Integer |]
-prove [t| Word |]
-prove [t| Double |]
-prove [t| Float |]
-prove [t| Char |]
-prove [t| Ordering |]
-prove [t| forall a. [a] |]
-prove [t| Rational |]
-prove [t| forall a. Maybe a |]
-prove [t| forall n. n :~: n |]
-prove [t| IsTrue 'True |]
+prove [t|Bool|]
+prove [t|Int|]
+prove [t|Integer|]
+prove [t|Word|]
+prove [t|Double|]
+prove [t|Float|]
+prove [t|Char|]
+prove [t|Ordering|]
+prove [t|forall a. [a]|]
+prove [t|Rational|]
+prove [t|forall a. Maybe a|]
+prove [t|forall n. n :~: n|]
+prove [t|IsTrue 'True|]
 
 instance Empty (IsTrue 'False) where
-  eliminate = \ case {}
+  eliminate = \case
diff --git a/Proof/Propositional/TH.hs b/Proof/Propositional/TH.hs
--- a/Proof/Propositional/TH.hs
+++ b/Proof/Propositional/TH.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE CPP, ExplicitNamespaces, MultiWayIf, PatternGuards #-}
-{-# LANGUAGE TemplateHaskell, TupleSections                     #-}
+{-# LANGUAGE TemplateHaskell, TupleSections, ViewPatterns                     #-}
 module Proof.Propositional.TH where
 import Proof.Propositional.Empty
 import Proof.Propositional.Inhabited
@@ -23,6 +23,10 @@
 #else
                                               DPat (DConPa, DVarPa), DPred(..),
 #endif
+#if MIN_VERSION_th_desugar(1,12,0)
+  DForallTelescope(..),
+#endif
+
                                               DTyVarBndr (..), DType (..),
                                               Overlap (Overlapping), desugar,
                                               dsReify, expandType, substTy,
@@ -30,7 +34,11 @@
 #if !MIN_VERSION_base(4,13,0)
 import           Data.Semigroup              (Semigroup (..))
 #endif
+#if MIN_VERSION_th_desugar(1,12,0)
+import Data.Functor (void)
+#endif
 
+
 -- | Macro to automatically derive @'Empty'@ instance for
 --   concrete (variable-free) types which may contain products.
 refute :: TypeQ -> DecsQ
@@ -181,14 +189,14 @@
 substFields subst (DRecC fs) =
   DRecC <$> forM fs (\(a,b,c) -> (a, b ,) <$> substTy subst c)
 
-dtvbToName :: DTyVarBndr -> Name
-dtvbToName (DPlainTV n)    = n
-dtvbToName (DKindedTV n _) = n
-
 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
@@ -246,7 +254,11 @@
   bd <- compareType' t s
   return (pd <> bd)
 compareType' DConstrainedT{} _ = return NonEqual
+#if MIN_VERSION_th_desugar(1,12,0)
+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
@@ -305,7 +317,11 @@
   | 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 _ _ = fail "Kind error: Expecting type-level predicate"
 #else
@@ -353,6 +369,19 @@
 substPred _ t = return t
 #endif
 
-
-
+{- FOURMOLU_DISABLE -}
+#if MIN_VERSION_th_desugar(1,12,0)
+dtvbToName :: DTyVarBndr flag -> Name
+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
@@ -2,7 +2,7 @@
 --  documentation, see http://haskell.org/cabal/users-guide/
 
 name:                equational-reasoning
-version:             0.6.0.4
+version:             0.7.0.0
 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.
@@ -13,7 +13,13 @@
 copyright:           (c) Hiromi ISHII 2013-2020
 category:            Math
 build-type:          Simple
-tested-with:         GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.1, GHC == 8.6.5, GHC == 8.8.2
+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.0.20201227
 cabal-version:       >=1.10
 source-repository head
     type: git