diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,4 +1,37 @@
-# Revision history for fin
+# Version history for fin
+
+## 0.3.2
+
+- Add `SS' :: SNat n -> SNat (S n)`, pattern synonym with explicit argument.
+
+## 0.3.1
+
+- Support GHC-8.6.5...9.10.1
+
+## 0.3
+
+- Remove `Data.Fin.Enum` module. It didn't work as well as hoped.
+- Add `EqP` and `OrdP` instances.
+- Add `GShow Fin` instance.
+
+## 0.2.1
+
+- Add `boring` instances
+- Explicitly implement `>=` and `>` for `Nat`.
+- `<=`, `>=` and `min` for `Nat` are lazier
+- Add `NFData (SNat n)` instance
+- Add `GEq`, `GCompare`, `GNFData`, `GShow` (from `some` package) instances for `SNat`.
+
+## 0.2
+
+- `SNat` is now what was called `InlineInduction`.
+  To migrate code from `fin-0.1` to `fin-0.2` it's often enough to
+  replace `InlineInduction` with `SNatI`, and `inlineInduction` with `induction`. 
+- Explicitly mark all modules as Safe or Trustworthy.
+
+## 0.1.2
+
+- Add `universe-base` `Universe` and `Finite` instances
 
 ## 0.1.1
 
diff --git a/fin.cabal b/fin.cabal
--- a/fin.cabal
+++ b/fin.cabal
@@ -1,6 +1,6 @@
-cabal-version:      >=1.10
+cabal-version:      2.2
 name:               fin
-version:            0.1.1
+version:            0.3.2
 synopsis:           Nat and Fin: peano naturals and finite numbers
 category:           Data, Dependent Types, Singletons, Math
 description:
@@ -48,21 +48,23 @@
 
 homepage:           https://github.com/phadej/vec
 bug-reports:        https://github.com/phadej/vec/issues
-license:            BSD3
+license:            BSD-3-Clause
 license-file:       LICENSE
 author:             Oleg Grenrus <oleg.grenrus@iki.fi>
 maintainer:         Oleg.Grenrus <oleg.grenrus@iki.fi>
-copyright:          (c) 2017-2019 Oleg Grenrus
+copyright:          (c) 2017-2021 Oleg Grenrus
 build-type:         Simple
 extra-source-files: ChangeLog.md
 tested-with:
-  GHC ==7.8.4
-   || ==7.10.3
-   || ==8.0.2
-   || ==8.2.2
-   || ==8.4.4
-   || ==8.6.5
-   || ==8.8.1
+  GHC ==8.6.5
+   || ==8.8.4
+   || ==8.10.7
+   || ==9.0.2
+   || ==9.2.8
+   || ==9.4.8
+   || ==9.6.5
+   || ==9.8.2
+   || ==9.10.1
 
 source-repository head
   type:     git
@@ -70,39 +72,39 @@
   subdir:   fin
 
 library
+  default-language: Haskell2010
+  ghc-options:      -Wall -fprint-explicit-kinds
+  hs-source-dirs:   src
   exposed-modules:
     Data.Fin
-    Data.Fin.Enum
     Data.Nat
     Data.Type.Nat
     Data.Type.Nat.LE
     Data.Type.Nat.LE.ReflStep
     Data.Type.Nat.LT
 
-  build-depends:
-      base        >=4.7     && <4.14
-    , dec         >=0.0.3   && <0.1
-    , deepseq     >=1.3.0.2 && <1.5
-    , hashable    >=1.2.7.0 && <1.4
-    , QuickCheck  >=2.13.2  && <2.14
-
-  if !impl(ghc >=8.2)
-    build-depends: bifunctors >=5.5.3 && <5.6
+  other-modules:    TrustworthyCompat
 
-  if !impl(ghc >=8.0)
-    build-depends: semigroups >=0.18.4 && <0.20
+  -- GHC boot libs
+  build-depends:
+    , base     >=4.12.0.0 && <4.21
+    , deepseq  >=1.4.4.0  && <1.6
 
-  if !impl(ghc >=7.10)
-    build-depends:
-        nats  >=1.1.2 && <1.2
-      , void  >=0.7.2 && <0.8
+  -- other dependencies
+  build-depends:
+    , boring         ^>=0.2.2
+    , dec            ^>=0.0.6
+    , hashable       ^>=1.4.4.0 || ^>=1.5.0.0
+    , QuickCheck     ^>=2.14.2  || ^>=2.15
+    , some           ^>=1.0.6
+    , universe-base  ^>=1.1.4
 
-  ghc-options:      -Wall -fprint-explicit-kinds
-  hs-source-dirs:   src
-  default-language: Haskell2010
+  if impl(ghc >=9.0)
+    -- these flags may abort compilation with GHC-8.10
+    -- https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3295
+    ghc-options: -Winferred-safe-imports -Wmissing-safe-haskell-mode
 
 -- dump-core
--- if impl(ghc >= 8.0)
 --  build-depends: dump-core
 --  ghc-options: -fplugin=DumpCore -fplugin-opt DumpCore:core-html
 
@@ -113,9 +115,9 @@
   hs-source-dirs:   test
   default-language: Haskell2010
   build-depends:
-      base
+    , base
     , fin
-    , inspection-testing  >=0.2.0.1 && <0.5
+    , inspection-testing  >=0.2.0.1 && <0.6
     , tagged
 
   if !impl(ghc >=8.0)
diff --git a/src/Data/Fin.hs b/src/Data/Fin.hs
--- a/src/Data/Fin.hs
+++ b/src/Data/Fin.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE EmptyCase            #-}
 {-# LANGUAGE GADTs                #-}
 {-# LANGUAGE KindSignatures       #-}
+{-# LANGUAGE Safe                 #-}
 {-# LANGUAGE ScopedTypeVariables  #-}
 {-# LANGUAGE StandaloneDeriving   #-}
 {-# LANGUAGE TypeOperators        #-}
@@ -52,18 +53,36 @@
 
 import Control.DeepSeq    (NFData (..))
 import Data.Bifunctor     (bimap)
+import Data.EqP           (EqP (..))
+import Data.GADT.Show     (GShow (..))
 import Data.Hashable      (Hashable (..))
 import Data.List.NonEmpty (NonEmpty (..))
+import Data.OrdP          (OrdP (..))
 import Data.Proxy         (Proxy (..))
 import Data.Type.Nat      (Nat (..))
 import Data.Typeable      (Typeable)
 import GHC.Exception      (ArithException (..), throw)
 import Numeric.Natural    (Natural)
 
-import qualified Data.List.NonEmpty as NE
-import qualified Data.Type.Nat      as N
-import qualified Test.QuickCheck    as QC
+import qualified Data.Boring           as Boring
+import qualified Data.List.NonEmpty    as NE
+import qualified Data.Type.Nat         as N
+import qualified Data.Universe.Class   as U
+import qualified Data.Universe.Helpers as U
+import qualified Test.QuickCheck       as QC
 
+-- $setup
+-- >>> import Data.List (genericLength)
+-- >>> import Data.List.NonEmpty (NonEmpty (..))
+-- >>> import Data.Foldable (traverse_)
+-- >>> import Numeric.Natural (Natural)
+-- >>> import qualified Data.Type.Nat as N
+-- >>> import qualified Data.Universe.Class as U
+-- >>> import qualified Data.Universe.Helpers as U
+-- >>> import Data.EqP (eqp)
+-- >>> import Data.OrdP (comparep)
+-- >>> :set -XTypeApplications -XGADTs
+
 -------------------------------------------------------------------------------
 -- Type
 -------------------------------------------------------------------------------
@@ -81,12 +100,53 @@
 deriving instance Eq (Fin n)
 deriving instance Ord (Fin n)
 
+-- |
+--
+-- >>> eqp FZ FZ
+-- True
+--
+-- >>> eqp FZ (FS FZ)
+-- False
+--
+-- >>> let xs = universe @N.Nat4; ys = universe @N.Nat6 in traverse_ print [ [ eqp x y | y <- ys ] | x <- xs ]
+-- [True,False,False,False,False,False]
+-- [False,True,False,False,False,False]
+-- [False,False,True,False,False,False]
+-- [False,False,False,True,False,False]
+--
+-- @since 0.2.2
+--
+instance EqP Fin where
+    eqp FZ     FZ     = True
+    eqp FZ     (FS _) = False
+    eqp (FS _) FZ     = False
+    eqp (FS n) (FS m) = eqp n m
+
+-- |
+--
+-- >>> let xs = universe @N.Nat4; ys = universe @N.Nat6 in traverse_ print [ [ comparep x y | y <- ys ] | x <- xs ]
+-- [EQ,LT,LT,LT,LT,LT]
+-- [GT,EQ,LT,LT,LT,LT]
+-- [GT,GT,EQ,LT,LT,LT]
+-- [GT,GT,GT,EQ,LT,LT]
+--
+-- @since 0.2.2
+instance OrdP Fin where
+    comparep FZ     FZ     = EQ
+    comparep FZ     (FS _) = LT
+    comparep (FS _) FZ     = GT
+    comparep (FS n) (FS m) = comparep n m
+
 -- | 'Fin' is printed as 'Natural'.
 --
 -- To see explicit structure, use 'explicitShow' or 'explicitShowsPrec'
 instance Show (Fin n) where
     showsPrec d  = showsPrec d . toNatural
 
+-- | @since 0.2.2
+instance GShow Fin where
+    gshowsPrec = showsPrec
+
 -- | Operations module @n@.
 --
 -- >>> map fromInteger [0, 1, 2, 3, 4, -5] :: [Fin N.Nat3]
@@ -143,14 +203,14 @@
 --
 -- @since 0.1.1
 --
-mirror :: forall n. N.InlineInduction n => Fin n -> Fin n
-mirror = getMirror (N.inlineInduction start step) where
+mirror :: forall n. N.SNatI n => Fin n -> Fin n
+mirror = getMirror (N.induction start step) where
     start :: Mirror 'Z
     start = Mirror id
 
-    step :: forall m. N.InlineInduction m => Mirror m -> Mirror ('S m)
+    step :: forall m. N.SNatI m => Mirror m -> Mirror ('S m)
     step (Mirror rec) = Mirror $ \n -> case n of
-        FZ   -> getMaxBound (N.inlineInduction (MaxBound FZ) (MaxBound . FS . getMaxBound))
+        FZ   -> getMaxBound (N.induction (MaxBound FZ) (MaxBound . FS . getMaxBound))
         FS m -> weakenLeft1 (rec m)
 
 newtype Mirror n = Mirror { getMirror :: Fin n -> Fin n }
@@ -202,6 +262,14 @@
     hashWithSalt salt = hashWithSalt salt . cata (0 :: Integer) succ
 
 -------------------------------------------------------------------------------
+-- Boring
+-------------------------------------------------------------------------------
+
+-- | @since 0.2.1
+instance n ~ 'Z => Boring.Absurd (Fin n) where
+    absurd = absurd
+
+-------------------------------------------------------------------------------
 -- QuickCheck
 -------------------------------------------------------------------------------
 
@@ -228,13 +296,32 @@
 
 instance (n ~ 'S m, N.SNatI m) => QC.Function (Fin n) where
     function = case N.snat :: N.SNat m of
-        N.SZ -> QC.functionMap (\FZ -> ()) (\() -> FZ)
-        N.SS -> QC.functionMap isMin       (maybe FZ FS)
+        N.SZ -> QC.functionMap (\_ -> ()) (\() -> FZ)
+        N.SS -> QC.functionMap isMin      (maybe FZ FS)
 
 -- TODO: https://github.com/nick8325/quickcheck/pull/283
 -- newtype Fun b m = Fun { getFun :: (Fin ('S m) -> b) -> Fin ('S m) QC.:-> b }
 
 -------------------------------------------------------------------------------
+-- universe-base
+-------------------------------------------------------------------------------
+
+-- | @since 0.1.2
+instance N.SNatI n => U.Universe (Fin n) where
+    universe = universe
+
+-- |
+--
+-- >>> (U.cardinality :: U.Tagged (Fin N.Nat3) Natural) == U.Tagged (genericLength (U.universeF :: [Fin N.Nat3]))
+-- True
+--
+-- @since 0.1.2
+--
+instance N.SNatI n => U.Finite   (Fin n) where
+    universeF   = U.universe
+    cardinality = U.Tagged $ N.reflectToNum (Proxy :: Proxy n)
+
+-------------------------------------------------------------------------------
 -- Showing
 -------------------------------------------------------------------------------
 
@@ -338,15 +425,15 @@
 --
 -- >>> inlineUniverse :: [Fin N.Nat3]
 -- [0,1,2]
-inlineUniverse :: N.InlineInduction n => [Fin n]
-inlineUniverse = getUniverse $ N.inlineInduction (Universe []) step where
+inlineUniverse :: N.SNatI n => [Fin n]
+inlineUniverse = getUniverse $ N.induction (Universe []) step where
     step :: Universe n -> Universe ('S n)
     step (Universe xs) = Universe (FZ : map FS xs)
 
 -- | >>> inlineUniverse1 :: NonEmpty (Fin N.Nat3)
 -- 0 :| [1,2]
-inlineUniverse1 :: N.InlineInduction n => NonEmpty (Fin ('S n))
-inlineUniverse1 = getUniverse1 $ N.inlineInduction (Universe1 (FZ :| [])) step where
+inlineUniverse1 :: N.SNatI n => NonEmpty (Fin ('S n))
+inlineUniverse1 = getUniverse1 $ N.induction (Universe1 (FZ :| [])) step where
     step :: Universe1 n -> Universe1 ('S n)
     step (Universe1 xs) = Universe1 (NE.cons FZ (fmap FS xs))
 
@@ -392,8 +479,8 @@
 --
 -- @since 0.1.1
 --
-isMax :: forall n. N.InlineInduction n => Fin ('S n) -> Maybe (Fin n)
-isMax = getIsMax (N.inlineInduction start step) where
+isMax :: forall n. N.SNatI n => Fin ('S n) -> Maybe (Fin n)
+isMax = getIsMax (N.induction start step) where
     start :: IsMax 'Z
     start = IsMax $ \_ -> Nothing
 
@@ -419,8 +506,8 @@
 -- [0,1,2,3]
 --
 -- @since 0.1.1
-weakenLeft1 :: N.InlineInduction n => Fin n -> Fin ('S n)
-weakenLeft1 = getWeaken1 (N.inlineInduction start step) where
+weakenLeft1 :: N.SNatI n => Fin n -> Fin ('S n)
+weakenLeft1 = getWeaken1 (N.induction start step) where
     start :: Weaken1 'Z
     start = Weaken1 absurd
 
@@ -433,8 +520,8 @@
 
 -- | >>> map (weakenLeft (Proxy :: Proxy N.Nat2)) (universe :: [Fin N.Nat3])
 -- [0,1,2]
-weakenLeft :: forall n m. N.InlineInduction n => Proxy m -> Fin n -> Fin (N.Plus n m)
-weakenLeft _ = getWeakenLeft (N.inlineInduction start step :: WeakenLeft m n) where
+weakenLeft :: forall n m. N.SNatI n => Proxy m -> Fin n -> Fin (N.Plus n m)
+weakenLeft _ = getWeakenLeft (N.induction start step :: WeakenLeft m n) where
     start :: WeakenLeft m 'Z
     start = WeakenLeft absurd
 
@@ -447,8 +534,8 @@
 
 -- | >>> map (weakenRight (Proxy :: Proxy N.Nat2)) (universe :: [Fin N.Nat3])
 -- [2,3,4]
-weakenRight :: forall n m. N.InlineInduction n => Proxy n -> Fin m -> Fin (N.Plus n m)
-weakenRight _ = getWeakenRight (N.inlineInduction start step :: WeakenRight m n) where
+weakenRight :: forall n m. N.SNatI n => Proxy n -> Fin m -> Fin (N.Plus n m)
+weakenRight _ = getWeakenRight (N.induction start step :: WeakenRight m n) where
     start = WeakenRight id
     step (WeakenRight go) = WeakenRight $ \x -> FS $ go x
 
@@ -462,7 +549,7 @@
 -- >>> append (Right fin2 :: Either (Fin N.Nat5) (Fin N.Nat4))
 -- 7
 --
-append :: forall n m. N.InlineInduction n => Either (Fin n) (Fin m) -> Fin (N.Plus n m)
+append :: forall n m. N.SNatI n => Either (Fin n) (Fin m) -> Fin (N.Plus n m)
 append (Left n)  = weakenLeft (Proxy :: Proxy m) n
 append (Right m) = weakenRight (Proxy :: Proxy n) m
 
@@ -477,8 +564,8 @@
 -- >>> map split universe :: [Either (Fin N.Nat2) (Fin N.Nat3)]
 -- [Left 0,Left 1,Right 0,Right 1,Right 2]
 --
-split :: forall n m. N.InlineInduction n => Fin (N.Plus n m) -> Either (Fin n) (Fin m)
-split = getSplit (N.inlineInduction start step) where
+split :: forall n m. N.SNatI n => Fin (N.Plus n m) -> Either (Fin n) (Fin m)
+split = getSplit (N.induction start step) where
     start :: Split m 'Z
     start = Split Right
 
diff --git a/src/Data/Fin/Enum.hs b/src/Data/Fin/Enum.hs
deleted file mode 100644
--- a/src/Data/Fin/Enum.hs
+++ /dev/null
@@ -1,170 +0,0 @@
-{-# LANGUAGE ConstraintKinds       #-}
-{-# LANGUAGE DataKinds             #-}
-{-# LANGUAGE DefaultSignatures     #-}
-{-# LANGUAGE FlexibleContexts      #-}
-{-# LANGUAGE FlexibleInstances     #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE PolyKinds             #-}
-{-# LANGUAGE ScopedTypeVariables   #-}
-{-# LANGUAGE TypeFamilies          #-}
-{-# LANGUAGE TypeOperators         #-}
-{-# LANGUAGE UndecidableInstances  #-}
--- |
---
--- This module is designed to be imported qualified:
---
--- @
--- import qualified Data.Fin.Enum as E
--- @
---
-module Data.Fin.Enum (
-    Enum (..),
-    -- * Generic implementation
-    gfrom, GFrom,
-    gto, GTo,
-    GEnumSize,
-    ) where
-
-import Prelude hiding (Enum (..))
-
-import Data.Bifunctor (bimap)
-import Data.Fin       (Fin (..))
-import Data.Nat       (Nat (..))
-import Data.Proxy     (Proxy (..))
-import GHC.Generics   ((:+:) (..), M1 (..), U1 (..), V1)
-
-import qualified Data.Fin      as F
-import qualified Data.Type.Nat as N
-import qualified Data.Void     as V
-import qualified GHC.Generics  as G
-
--- | Generic enumerations.
---
--- /Examples:/
---
--- >>> from ()
--- 0
---
--- >>> to 0 :: ()
--- ()
---
--- >>> to 0 :: Bool
--- False
---
--- >>> map to F.universe :: [Bool]
--- [False,True]
---
--- >>> map (to . (+1) . from) [LT, EQ, GT] :: [Ordering] -- Num Fin is modulo arithmetic
--- [EQ,GT,LT]
---
-class Enum a where
-    -- | The size of an enumeration.
-    type EnumSize a :: Nat
-    type EnumSize a = GEnumSize a
-
-    -- | Converts a value to its index.
-    from :: a -> Fin (EnumSize a)
-    default from :: (G.Generic a, GFrom a, EnumSize a ~ GEnumSize a) => a -> Fin (EnumSize a)
-    from = gfrom
-
-    -- | Converts from index to the original value.
-    to :: Fin (EnumSize a) -> a
-    default to :: (G.Generic a, GTo a, EnumSize a ~ GEnumSize a) => Fin (EnumSize a) -> a
-    to = gto
-
--- | 'Void' ~ 0
-instance Enum V.Void where
-    -- this should be written by hand to work with all @base@
-    type EnumSize V.Void = N.Nat0
-    from = V.absurd
-    to   = F.absurd
-
--- | () ~ 1
-instance Enum ()
-
--- | 'Bool' ~ 2
-instance Enum Bool
-
--- | 'Ordering' ~ 3
-instance Enum Ordering
-
--- | 'Either' ~ @+@
-instance (Enum a, Enum b, N.InlineInduction (EnumSize a)) => Enum (Either a b) where
-    type EnumSize (Either a b) = N.Plus (EnumSize a) (EnumSize b)
-
-    to   = bimap to to . F.split
-    from = F.append . bimap from from
-
--------------------------------------------------------------------------------
--- EnumSize
--------------------------------------------------------------------------------
-
--- | Compute the size from the type.
-type GEnumSize a = EnumSizeRep (G.Rep a) N.Nat0
-
-type family EnumSizeRep (a :: * -> *) (n :: Nat) :: Nat where
-    EnumSizeRep (a :+: b )   n = EnumSizeRep a (EnumSizeRep b n)
-    EnumSizeRep V1           n = n
-    EnumSizeRep (M1 _d _c a) n = EnumSizeRep a n
-    EnumSizeRep U1           n = 'S n
-    -- No instance for K1 or :*:
-
--------------------------------------------------------------------------------
--- From
--------------------------------------------------------------------------------
-
--- | Generic version of 'from'.
-gfrom :: (G.Generic a, GFrom a) => a -> Fin (GEnumSize a)
-gfrom = \x -> gfromRep (G.from x) (error "gfrom: internal error" :: Fin N.Nat0)
-
--- | Constraint for the class that computes 'gfrom'.
-type GFrom a = GFromRep (G.Rep a)
-
-class GFromRep (a :: * -> *)  where
-    gfromRep  :: a x     -> Fin n -> Fin (EnumSizeRep a n)
-    gfromSkip :: Proxy a -> Fin n -> Fin (EnumSizeRep a n)
-
-instance (GFromRep a, GFromRep b) => GFromRep (a :+: b) where
-    gfromRep (L1 a) n = gfromRep a (gfromSkip (Proxy :: Proxy b) n)
-    gfromRep (R1 b) n = gfromSkip (Proxy :: Proxy a) (gfromRep b n)
-
-    gfromSkip _ n = gfromSkip (Proxy :: Proxy a) (gfromSkip (Proxy :: Proxy b) n)
-
-instance GFromRep a => GFromRep (M1 d c a) where
-    gfromRep (M1 a) n = gfromRep a n
-    gfromSkip _     n = gfromSkip (Proxy :: Proxy a) n
-
-instance GFromRep V1 where
-    gfromRep  _ n = n
-    gfromSkip _ n = n
-
-instance GFromRep U1 where
-    gfromRep U1 _ = FZ
-    gfromSkip _ n = FS n
-
--------------------------------------------------------------------------------
--- To
--------------------------------------------------------------------------------
-
--- | Generic version of 'to'.
-gto :: (G.Generic a, GTo a) => Fin (GEnumSize a) -> a
-gto = \x -> G.to $ gtoRep x id F.absurd
-
--- | Constraint for the class that computes 'gto'.
-type GTo a = GToRep (G.Rep a)
-
-class GToRep (a :: * -> *) where
-    gtoRep :: Fin (EnumSizeRep a n) -> (a x -> r) -> (Fin n -> r) -> r
-
-instance (GToRep a, GToRep b) => GToRep (a :+: b) where
-    gtoRep n s k = gtoRep n (s . L1) $ \r -> gtoRep r (s . R1) k
-
-instance GToRep a => GToRep (M1 d c a) where
-    gtoRep n s = gtoRep n (s . M1)
-
-instance GToRep V1 where
-    gtoRep n _ k = k n
-
-instance GToRep U1 where
-    gtoRep FZ     s _ = s U1
-    gtoRep (FS n) _ k = k n
diff --git a/src/Data/Nat.hs b/src/Data/Nat.hs
--- a/src/Data/Nat.hs
+++ b/src/Data/Nat.hs
@@ -1,10 +1,6 @@
 {-# LANGUAGE CPP                #-}
 {-# LANGUAGE DeriveDataTypeable #-}
-
-#if __GLASGOW_HASKELL__ < 710
-{-# LANGUAGE DataKinds          #-}
-{-# LANGUAGE StandaloneDeriving #-}
-#endif
+{-# LANGUAGE Safe               #-}
 -- | 'Nat' numbers.
 --
 -- This module is designed to be imported qualified.
@@ -29,8 +25,11 @@
 import GHC.Exception   (ArithException (..), throw)
 import Numeric.Natural (Natural)
 
-import qualified Test.QuickCheck as QC
+import qualified Data.Universe.Class as U
+import qualified Test.QuickCheck     as QC
 
+-- $setup
+
 -------------------------------------------------------------------------------
 -- Nat
 -------------------------------------------------------------------------------
@@ -39,12 +38,7 @@
 --
 -- Better than GHC's built-in 'GHC.TypeLits.Nat' for some use cases.
 --
-data Nat = Z | S Nat deriving (Eq, Ord, Typeable, Data)
-
-#if __GLASGOW_HASKELL__ < 710
-deriving instance Typeable 'Z
-deriving instance Typeable 'S
-#endif
+data Nat = Z | S Nat deriving (Eq, Typeable, Data)
 
 -- | 'Nat' is printed as 'Natural'.
 --
@@ -53,6 +47,29 @@
 instance Show Nat where
     showsPrec d = showsPrec d . toNatural
 
+instance Ord Nat where
+    compare Z     Z     = EQ
+    compare Z     (S _) = LT
+    compare (S _) Z     = GT
+    compare (S n) (S m) = compare n m
+
+    Z   <= _   = True
+    S _ <= Z   = False
+    S n <= S m = n <= m
+
+    n <  m = not (m <= n)
+    n >  m = not (n <= m)
+    n >= m = m <= n
+
+    min Z     _     = Z
+    min (S _) Z     = Z
+    min (S n) (S m) = S (min n m)
+
+    max Z       Z       = Z
+    max Z       m@(S _) = m
+    max n@(S _) Z       = n
+    max (S n)   (S m)   = S (max n m)
+
 instance Num Nat where
     fromInteger = fromNatural . fromInteger
 
@@ -114,11 +131,26 @@
     shrink (S n) = n : QC.shrink n
 
 instance QC.CoArbitrary Nat where
-    coarbitrary Z     = QC.variant (0 :: Int) 
+    coarbitrary Z     = QC.variant (0 :: Int)
     coarbitrary (S n) = QC.variant (1 :: Int) . QC.coarbitrary n
 
 instance QC.Function Nat where
     function = QC.functionIntegral
+
+-------------------------------------------------------------------------------
+-- universe-base
+-------------------------------------------------------------------------------
+
+-- |
+--
+-- >>> import qualified Data.Universe.Class as U
+-- >>> take 10 (U.universe :: [Nat])
+-- [0,1,2,3,4,5,6,7,8,9]
+--
+-- @since 0.1.2
+instance U.Universe Nat where
+    universe = go Z where
+        go n = n : go (S n)
 
 -------------------------------------------------------------------------------
 -- Showing
diff --git a/src/Data/Type/Nat.hs b/src/Data/Type/Nat.hs
--- a/src/Data/Type/Nat.hs
+++ b/src/Data/Type/Nat.hs
@@ -1,15 +1,17 @@
-{-# LANGUAGE CPP                  #-}
 {-# LANGUAGE DataKinds            #-}
 {-# LANGUAGE DeriveDataTypeable   #-}
 {-# LANGUAGE EmptyCase            #-}
 {-# LANGUAGE GADTs                #-}
 {-# LANGUAGE KindSignatures       #-}
+{-# LANGUAGE PatternSynonyms      #-}
 {-# LANGUAGE RankNTypes           #-}
 {-# LANGUAGE ScopedTypeVariables  #-}
 {-# LANGUAGE StandaloneDeriving   #-}
+{-# LANGUAGE Trustworthy          #-}
 {-# LANGUAGE TypeFamilies         #-}
 {-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ViewPatterns         #-}
 -- | 'Nat' numbers. @DataKinds@ stuff.
 --
 -- This module re-exports "Data.Nat", and adds type-level things.
@@ -23,11 +25,12 @@
     explicitShow,
     explicitShowsPrec,
     -- * Singleton
-    SNat(..),
+    SNat(SZ,SS,SS'),
     snatToNat,
     snatToNatural,
     -- * Implicit
     SNatI(..),
+    snat,
     withSNat,
     reify,
     reflect,
@@ -36,11 +39,9 @@
     eqNat,
     EqNat,
     discreteNat,
+    cmpNat,
     -- * Induction
-    induction,
     induction1,
-    InlineInduction (..),
-    inlineInduction,
     -- ** Example: unfoldedFix
     unfoldedFix,
     -- * Arithmetic
@@ -65,26 +66,34 @@
     proofMultNOne,
     )  where
 
-import Data.Function      (fix)
-import Data.Proxy         (Proxy (..))
-import Data.Type.Dec      (Dec (..))
-import Data.Type.Equality ((:~:) (..), TestEquality (..))
-import Data.Typeable      (Typeable)
-import Numeric.Natural    (Natural)
+import Control.DeepSeq   (NFData (..))
+import Data.Boring       (Boring (..))
+import Data.EqP          (EqP (..))
+import Data.Function     (fix)
+import Data.GADT.Compare (GCompare (..), GEq (..), GOrdering (..), defaultCompare, defaultEq)
+import Data.GADT.DeepSeq (GNFData (..))
+import Data.GADT.Show    (GShow (..))
+import Data.OrdP         (OrdP (..))
+import Data.Proxy        (Proxy (..))
+import Data.Type.Dec     (Dec (..))
+import Data.Typeable     (Typeable)
+import Numeric.Natural   (Natural)
 
 import qualified GHC.TypeLits as GHC
 
 import Unsafe.Coerce (unsafeCoerce)
 
-#if !MIN_VERSION_base(4,11,0)
-import Data.Type.Equality (type (==))
-#endif
-
 import Data.Nat
+import TrustworthyCompat
 
 -- $setup
 -- >>> :set -XTypeOperators -XDataKinds
--- >>> import Data.Type.Dec (decShow)
+-- >>> import qualified GHC.TypeLits as GHC
+-- >>> import Data.Type.Dec (Dec (..), decShow)
+-- >>> import Data.Type.Equality
+-- >>> import Control.Applicative (Const (..))
+-- >>> import Data.Coerce (coerce)
+-- >>> import Data.GADT.Compare (GOrdering (..))
 
 -------------------------------------------------------------------------------
 -- SNat
@@ -98,11 +107,34 @@
 
 deriving instance Show (SNat p)
 
--- | Convenience class to get 'SNat'.
-class               SNatI (n :: Nat) where snat :: SNat n
-instance            SNatI 'Z         where snat = SZ
-instance SNatI n => SNatI ('S n)     where snat = SS
+-- | Implicit 'SNat'.
+--
+-- In an unorthodox singleton way, it actually provides an induction function.
+--
+-- The induction should often be fully inlined.
+-- See @test/Inspection.hs@.
+--
+-- >>> :set -XPolyKinds
+-- >>> newtype Const a b = Const a deriving (Show)
+-- >>> induction (Const 0) (coerce ((+2) :: Int -> Int)) :: Const Int Nat3
+-- Const 6
+--
+class SNatI (n :: Nat) where
+    induction
+        :: f 'Z                                    -- ^ zero case
+        -> (forall m. SNatI m => f m -> f ('S m))  -- ^ induction step
+        -> f n
 
+instance SNatI 'Z where
+    induction n _c = n
+
+instance SNatI n => SNatI ('S n) where
+    induction n c = c (induction n c)
+
+-- | Construct explicit 'SNat' value.
+snat :: SNatI n => SNat n
+snat = induction SZ (\_ -> SS)
+
 -- | Constructor 'SNatI' dictionary from 'SNat'.
 --
 -- @since 0.0.3
@@ -112,11 +144,11 @@
 
 -- | Reflect type-level 'Nat' to the term level.
 reflect :: forall n proxy. SNatI n => proxy n -> Nat
-reflect _ = unTagged (induction1 (Tagged Z) (retagMap S) :: Tagged n Nat)
+reflect _ = unKonst (induction (Konst Z) (kmap S) :: Konst Nat n)
 
 -- | As 'reflect' but with any 'Num'.
 reflectToNum :: forall n m proxy. (SNatI n, Num m) => proxy n -> m
-reflectToNum _ = unTagged (induction1 (Tagged 0) (retagMap (1+)) :: Tagged n m)
+reflectToNum _ = unKonst (induction (Konst 0) (kmap (1+)) :: Konst m n)
 
 -- | Reify 'Nat'.
 --
@@ -133,7 +165,7 @@
 --
 snatToNat :: forall n. SNat n -> Nat
 snatToNat SZ = Z
-snatToNat SS = unTagged (induction1 (Tagged Z) (retagMap S) :: Tagged n Nat)
+snatToNat SS = unKonst (induction (Konst Z) (kmap S) :: Konst Nat n)
 
 -- | Convert 'SNat' to 'Natural'
 --
@@ -145,9 +177,38 @@
 --
 snatToNatural :: forall n. SNat n -> Natural
 snatToNatural SZ = 0
-snatToNatural SS = unTagged (induction1 (Tagged 0) (retagMap succ) :: Tagged n Natural)
+snatToNatural SS = unKonst (induction (Konst 0) (kmap succ) :: Konst Natural n)
 
 -------------------------------------------------------------------------------
+-- Explicit constructor
+-------------------------------------------------------------------------------
+
+data SNat_ (n :: Nat) where
+    SZ_ :: SNat_ 'Z
+    SS_ :: SNat n -> SNat_ ('S n)
+
+snat_ :: SNat n -> SNat_ n
+snat_ SZ = SZ_
+snat_ SS = SS_ snat
+
+-- | A pattern with explicit argument
+--
+-- >>> let predSNat :: SNat (S n) -> SNat n; predSNat (SS' n) = n
+-- >>> predSNat (SS' (SS' SZ))
+-- SS
+--
+-- >>> reflect $ predSNat (SS' (SS' SZ))
+-- 1
+--
+--
+-- @since 0.3.2
+pattern SS' :: () => (m ~ 'S n) => SNat n -> SNat m
+pattern SS' n <- (snat_ -> SS_ n)
+  where SS' n = withSNat n SS
+
+{-# COMPLETE SZ, SS' #-}
+
+-------------------------------------------------------------------------------
 -- Equality
 -------------------------------------------------------------------------------
 
@@ -216,76 +277,100 @@
     EqNat ('S n) ('S m) = EqNat n m
     EqNat n      m      = 'False
 
-#if !MIN_VERSION_base(4,11,0)
-type instance n == m = EqNat n m
-#endif
+-- | @since 0.2.1
+instance SNatI n => Boring (SNat n) where
+    boring = snat
 
+-- | @since 0.2.1
+instance GShow SNat where
+    gshowsPrec = showsPrec
+
+-- | @since 0.2.1
+instance NFData (SNat n) where
+    rnf SZ = ()
+    rnf SS = ()
+
+-- | @since 0.2.1
+instance GNFData SNat where
+    grnf = rnf
+
+
+-- | @since 0.2.1
+instance GEq SNat where
+    geq = testEquality
+
+-- | @since 0.2.1
+instance GCompare SNat where
+    gcompare SZ SZ = GEQ
+    gcompare SZ SS = GLT
+    gcompare SS SZ = GGT
+    gcompare SS SS = cmpNat
+
+-- | @since 0.2.2
+instance Eq (SNat a) where
+    _ == _ = True
+
+-- | @since 0.2.2
+instance Ord (SNat a) where
+    compare _ _ = EQ
+
+-- | @since 0.2.2
+instance EqP SNat where eqp = defaultEq
+
+-- | @since 0.2.2
+instance OrdP SNat where comparep = defaultCompare
+
+-- | Decide equality of type-level numbers.
+--
+-- >>> cmpNat :: GOrdering Nat3 (Plus Nat1 Nat2)
+-- GEQ
+--
+-- >>> cmpNat :: GOrdering Nat3 (Mult Nat2 Nat2)
+-- GLT
+--
+-- >>> cmpNat :: GOrdering Nat5 (Mult Nat2 Nat2)
+-- GGT
+--
+cmpNat :: forall n m. (SNatI n, SNatI m) => GOrdering n m
+cmpNat = getNatCmp $ induction (NatCmp start) (\p -> NatCmp (step p)) where
+    start :: forall p. SNatI p => GOrdering 'Z p
+    start = case snat :: SNat p of
+        SZ -> GEQ
+        SS -> GLT
+
+    step :: forall p q. SNatI q => NatCmp p -> GOrdering ('S p) q
+    step hind = case snat :: SNat q of
+        SZ -> GGT
+        SS -> step' hind
+
+    step' :: forall p q. SNatI q => NatCmp p -> GOrdering ('S p) ('S q)
+    step' (NatCmp hind) = case hind :: GOrdering p q of
+        GEQ -> GEQ
+        GLT -> GLT
+        GGT -> GGT
+
+newtype NatCmp n = NatCmp { getNatCmp :: forall m. SNatI m => GOrdering n m }
+
 -------------------------------------------------------------------------------
 -- Induction
 -------------------------------------------------------------------------------
 
+newtype Konst a (n :: Nat) = Konst { unKonst :: a }
+
+kmap :: (a -> b) -> Konst a n -> Konst b m
+kmap = coerce
+
+newtype Flipped f a (b :: Nat) = Flip { unflip :: f b a }
+
 -- | Induction on 'Nat', functor form. Useful for computation.
 --
--- >>> induction1 (Tagged 0) $ retagMap (+2) :: Tagged Nat3 Int
--- Tagged 6
---
 induction1
     :: forall n f a. SNatI n
     => f 'Z a                                      -- ^ zero case
     -> (forall m. SNatI m => f m a -> f ('S m) a)  -- ^ induction step
     -> f n a
-induction1 z f = go where
-    go :: forall m. SNatI m => f m a
-    go = case snat :: SNat m of
-        SZ -> z
-        SS -> f go
-
--- | Induction on 'Nat'.
---
--- Useful in proofs or with GADTs, see source of 'proofPlusNZero'.
-induction
-    :: forall n f. SNatI n
-    => f 'Z                                    -- ^ zero case
-    -> (forall m. SNatI m => f m -> f ('S m))  -- ^ induction step
-    -> f n
-induction z f = go where
-    go :: forall m. SNatI m => f m
-    go = case snat :: SNat m of
-        SZ -> z
-        SS -> f go
-
--- | The induction will be fully inlined.
---
--- See @test/Inspection.hs@.
-class SNatI n => InlineInduction (n :: Nat) where
-    inlineInduction1 :: f 'Z a -> (forall m. InlineInduction m => f m a -> f ('S m) a) -> f n a
-
-instance InlineInduction 'Z where
-    inlineInduction1 z _ = z
-
-instance InlineInduction n => InlineInduction ('S n) where
-    inlineInduction1 z f = f (inlineInduction1 z f)
-
-    -- Specialise this to few first numerals.
-    {-# SPECIALIZE instance InlineInduction ('S 'Z) #-}
-    {-# SPECIALIZE instance InlineInduction ('S ('S 'Z)) #-}
-    {-# SPECIALIZE instance InlineInduction ('S ('S ('S 'Z))) #-}
-    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S 'Z)))) #-}
-    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S 'Z))))) #-}
-    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S ('S 'Z)))))) #-}
-    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S ('S ('S 'Z))))))) #-}
-    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))) #-}
-    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))) #-}
-
--- | See 'InlineInduction'.
-inlineInduction
-    :: forall n f. InlineInduction n
-    => f 'Z                                              -- ^ zero case
-    -> (forall m. InlineInduction m => f m -> f ('S m))  -- ^ induction step
-    -> f n
-inlineInduction z f = unConst' $ inlineInduction1 (Const' z) (Const' . f . unConst')
-
-newtype Const' (f :: Nat -> *) (n :: Nat) a = Const' { unConst' :: f n }
+induction1 z f = unflip (induction (Flip z) (\(Flip x) -> Flip (f x)))
+{-# INLINE induction1 #-}
 
 -- | Unfold @n@ steps of a general recursion.
 --
@@ -298,15 +383,15 @@
 -- 'unfoldedFix' ('Proxy' :: 'Proxy' 'Nat3') f = f (f (f (fix f)))
 -- @
 --
-unfoldedFix :: forall n a proxy. InlineInduction n => proxy n -> (a -> a) -> a
-unfoldedFix _ = getFix (inlineInduction1 start step :: Fix n a) where
-    start :: Fix 'Z a
+unfoldedFix :: forall n a proxy. SNatI n => proxy n -> (a -> a) -> a
+unfoldedFix _ = getFix (induction start step :: Fix a n) where
+    start :: Fix a 'Z
     start = Fix fix
 
-    step :: Fix m a -> Fix ('S m) a
+    step :: Fix a m -> Fix a ('S m)
     step (Fix go) = Fix $ \f -> f (go f)
 
-newtype Fix (n :: Nat) a = Fix { getFix :: (a -> a) -> a }
+newtype Fix a (n :: Nat) = Fix { getFix :: (a -> a) -> a }
 
 -------------------------------------------------------------------------------
 -- Conversion to GHC Nat
@@ -315,7 +400,7 @@
 -- | Convert to GHC 'GHC.Nat'.
 --
 -- >>> :kind! ToGHC Nat5
--- ToGHC Nat5 :: GHC.Nat
+-- ToGHC Nat5 :: GHC.Nat...
 -- = 5
 --
 type family ToGHC (n :: Nat) :: GHC.Nat where
@@ -363,13 +448,13 @@
 
 -- | Division by two. 'False' is 0 and 'True' is 1 as a remainder.
 --
--- >>> :kind! DivMod2 Nat7
--- DivMod2 Nat7 :: (Nat, Bool)
--- = '( 'S ('S ('S 'Z)), 'True)
+-- >>> :kind! DivMod2 Nat7 == '(Nat3, True)
+-- DivMod2 Nat7 == '(Nat3, True) :: Bool
+-- = 'True
 --
--- >>> :kind! DivMod2 Nat4
--- DivMod2 Nat4 :: (Nat, Bool)
--- = '( 'S ('S 'Z), 'False)
+-- >>> :kind! DivMod2 Nat4 == '(Nat2, False)
+-- DivMod2 Nat4 == '(Nat2, False) :: Bool
+-- = 'True
 --
 type family DivMod2 (n :: Nat) :: (Nat, Bool) where
     DivMod2 'Z          = '( 'Z, 'False)
@@ -451,18 +536,3 @@
 newtype ProofMultNOne n = ProofMultNOne { getProofMultNOne :: Mult n Nat1 :~: n }
 
 -- TODO: multAssoc
-
--------------------------------------------------------------------------------
--- Tagged
--------------------------------------------------------------------------------
-
--- Own 'Tagged', to not depend on @tagged@
---
--- We shouldn't export this in public interface.
-newtype Tagged (n :: Nat) a = Tagged a deriving Show
-
-unTagged :: Tagged n a -> a
-unTagged (Tagged a) = a
-
-retagMap :: (a -> b) -> Tagged n a -> Tagged m b
-retagMap f = Tagged . f . unTagged
diff --git a/src/Data/Type/Nat/LE.hs b/src/Data/Type/Nat/LE.hs
--- a/src/Data/Type/Nat/LE.hs
+++ b/src/Data/Type/Nat/LE.hs
@@ -6,6 +6,7 @@
 {-# LANGUAGE GADTs                 #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE Safe                  #-}
 {-# LANGUAGE ScopedTypeVariables   #-}
 {-# LANGUAGE StandaloneDeriving    #-}
 {-# LANGUAGE TypeOperators         #-}
@@ -48,13 +49,16 @@
     proofZeroLEZero,
     ) where
 
-import Data.Type.Dec      (Dec (..), Decidable (..), Neg)
-import Data.Type.Equality ((:~:) (..))
-import Data.Typeable      (Typeable)
-import Data.Void          (absurd)
+import Data.Boring   (Boring (..), Absurd (..))
+import Data.Type.Dec (Dec (..), Decidable (..), Neg)
+import Data.Typeable (Typeable)
 
 import Data.Type.Nat
+import TrustworthyCompat
 
+-- $setup
+-- >>> import Data.Type.Nat
+
 -------------------------------------------------------------------------------
 -- Proof
 -------------------------------------------------------------------------------
@@ -158,6 +162,18 @@
 --
 leSwap' :: LEProof n m -> LEProof ('S m) n -> void
 leSwap' p (LESucc q) = case p of LESucc p' -> leSwap' p' q
+
+-------------------------------------------------------------------------------
+-- Boring
+-------------------------------------------------------------------------------
+
+-- | @since 0.2.1
+instance LE n m => Boring (LEProof n m) where
+    boring = leProof
+
+-- | @since 0.2.1
+instance (LE m n, n' ~ 'S n) => Absurd (LEProof n' m) where
+    absurd = leSwap' leProof
 
 -------------------------------------------------------------------------------
 -- Dedidablity
diff --git a/src/Data/Type/Nat/LE/ReflStep.hs b/src/Data/Type/Nat/LE/ReflStep.hs
--- a/src/Data/Type/Nat/LE/ReflStep.hs
+++ b/src/Data/Type/Nat/LE/ReflStep.hs
@@ -5,6 +5,7 @@
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE GADTs                 #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE Safe                  #-}
 {-# LANGUAGE ScopedTypeVariables   #-}
 {-# LANGUAGE StandaloneDeriving    #-}
 {-# LANGUAGE TypeOperators         #-}
@@ -35,14 +36,16 @@
     proofZeroLEZero,
     ) where
 
-import Data.Type.Dec      (Dec (..), Decidable (..), Neg)
-import Data.Type.Equality ((:~:) (..))
-import Data.Typeable      (Typeable)
-import Data.Void          (absurd)
+import Data.Boring   (Absurd (..), Boring (..))
+import Data.Type.Dec (Dec (..), Decidable (..), Neg)
+import Data.Typeable (Typeable)
 
-import Data.Type.Nat
-import qualified Data.Type.Nat.LE as ZeroSucc
+import qualified Control.Category as C
 
+import           Data.Type.Nat
+import qualified Data.Type.Nat.LE  as ZeroSucc
+import           TrustworthyCompat
+
 -------------------------------------------------------------------------------
 -- Proof
 -------------------------------------------------------------------------------
@@ -62,6 +65,12 @@
 instance Ord (LEProof n m) where
     compare _ _ = EQ
 
+-- | The other variant ('Data.Type.Nat.LE.LEPRoof') isn't 'C.Category',
+-- because 'Data.Type.Nat.LE.leRefl` requires 'SNat' evidence.
+instance C.Category LEProof where
+    id  = leRefl
+    (.) = flip leTrans
+
 -------------------------------------------------------------------------------
 -- Conversion
 -------------------------------------------------------------------------------
@@ -141,6 +150,18 @@
 leSwap' :: LEProof n m -> LEProof ('S m) n -> void
 leSwap' p LERefl     = case p of LEStep p' -> leSwap' (leStepL p') LERefl
 leSwap' p (LEStep q) = leSwap' (leStepL p) q
+
+-------------------------------------------------------------------------------
+-- Boring
+-------------------------------------------------------------------------------
+
+-- | @since 0.2.1
+instance (ZeroSucc.LE n m, SNatI m) => Boring (LEProof n m) where
+    boring = fromZeroSucc ZeroSucc.leProof
+
+-- | @since 0.2.1
+instance (ZeroSucc.LE m n, n' ~ 'S n, SNatI n) => Absurd (LEProof n' m) where
+    absurd = ZeroSucc.leSwap' ZeroSucc.leProof . toZeroSucc
 
 -------------------------------------------------------------------------------
 -- Decidability
diff --git a/src/Data/Type/Nat/LT.hs b/src/Data/Type/Nat/LT.hs
--- a/src/Data/Type/Nat/LT.hs
+++ b/src/Data/Type/Nat/LT.hs
@@ -4,6 +4,7 @@
 {-# LANGUAGE GADTs                 #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE Safe                  #-}
 {-# LANGUAGE TypeFamilies          #-}
 {-# LANGUAGE TypeOperators         #-}
 {-# LANGUAGE UndecidableInstances  #-}
@@ -19,6 +20,9 @@
 
 import Data.Type.Nat
 import Data.Type.Nat.LE
+
+-- $setup
+-- >>> import Data.Type.Nat
 
 -- | An evidence \(n < m\) which is the same as (\1 + n \le m\).
 type LTProof n m = LEProof ('S n) m
diff --git a/src/TrustworthyCompat.hs b/src/TrustworthyCompat.hs
new file mode 100644
--- /dev/null
+++ b/src/TrustworthyCompat.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE Trustworthy        #-}
+module TrustworthyCompat (
+    (:~:) (..),
+    TestEquality (..),
+    coerce,
+    type (==),
+) where
+
+import Data.Coerce        (coerce)
+import Data.Type.Equality (TestEquality (..), type (==), (:~:) (..))
diff --git a/test/Inspection.hs b/test/Inspection.hs
--- a/test/Inspection.hs
+++ b/test/Inspection.hs
@@ -1,5 +1,7 @@
+{-# LANGUAGE DataKinds           #-}
 {-# LANGUAGE DeriveGeneric       #-}
 {-# LANGUAGE GADTs               #-}
+{-# LANGUAGE RankNTypes          #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TemplateHaskell     #-}
 {-# LANGUAGE TypeOperators       #-}
@@ -15,23 +17,34 @@
 import Test.Inspection
 
 import qualified Data.Fin      as F
-import qualified Data.Fin.Enum as E
 import qualified Data.Type.Nat as N
 
 import Unsafe.Coerce (unsafeCoerce)
 
 -------------------------------------------------------------------------------
--- InlineInduction
+-- SNatI
 -------------------------------------------------------------------------------
 
 -- | This doesn't evaluate compile time.
 lhsInline :: Int
-lhsInline = unTagged (N.inlineInduction1 (pure 0) (retag . fmap succ) :: Tagged N.Nat5 Int)
+lhsInline = unTagged (N.induction1 (pure 0) (retag . fmap succ) :: Tagged N.Nat5 Int)
 
 -- | This doesn't evaluate compile time.
 lhsNormal :: Int
-lhsNormal = unTagged (N.induction1 (pure 0) (retag . fmap succ) :: Tagged N.Nat5 Int)
+lhsNormal = unTagged (manualInduction1 (pure 0) (retag . fmap succ) :: Tagged N.Nat5 Int)
 
+--- | Induction on 'Nat'.
+manualInduction1
+     :: forall n f a. N.SNatI n
+     => f 'N.Z a                                        -- ^ zero case
+     -> (forall m. N.SNatI m => f m a -> f ('N.S m) a)  -- ^ induction step
+     -> f n a
+manualInduction1 z f = go where
+    go :: forall m. N.SNatI m => f m a
+    go = case N.snat :: N.SNat m of
+        N.SZ -> z
+        N.SS -> f go
+
 rhs :: Int
 rhs = 5
 
@@ -39,26 +52,6 @@
 inspect $ 'lhsNormal =/= 'rhs
 
 -------------------------------------------------------------------------------
--- Enum
--------------------------------------------------------------------------------
-
--- | Note: GHC 8.0 (but not GHC 8.2?) seems to be
--- so smart, it reuses dictionary value.
---
--- Therefore, we define own local Ordering'
-data Ordering' = LT' | EQ' | GT' deriving (Generic)
-
-lhsEnum :: Ordering' -> F.Fin N.Nat3
-lhsEnum = E.gfrom
-
-rhsEnum :: Ordering' -> F.Fin N.Nat3
-rhsEnum LT' = FZ
-rhsEnum EQ' = FS FZ
-rhsEnum GT' = FS (FS FZ)
-
-inspect $ 'lhsEnum ==- 'rhsEnum
-
--------------------------------------------------------------------------------
 -- Proofs
 -------------------------------------------------------------------------------
 
@@ -110,10 +103,10 @@
 -- Power
 -------------------------------------------------------------------------------
 
-power :: forall n. N.InlineInduction n => Proxy n -> Int -> Int
+power :: forall n. N.SNatI n => Proxy n -> Int -> Int
 power _ k = unTagged impl where
     impl :: Tagged n Int
-    impl = N.inlineInduction1 (Tagged 1) $ \(Tagged rec') -> Tagged (rec' * k)
+    impl = N.induction1 (Tagged 1) $ \(Tagged rec') -> Tagged (rec' * k)
 
 lhsPower5 :: Int -> Int
 lhsPower5 = power (Proxy :: Proxy N.Nat5)