diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,9 @@
 # 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
diff --git a/fin.cabal b/fin.cabal
--- a/fin.cabal
+++ b/fin.cabal
@@ -1,6 +1,6 @@
 cabal-version:      2.2
 name:               fin
-version:            0.3.1
+version:            0.3.2
 synopsis:           Nat and Fin: peano naturals and finite numbers
 category:           Data, Dependent Types, Singletons, Math
 description:
@@ -94,7 +94,7 @@
   build-depends:
     , boring         ^>=0.2.2
     , dec            ^>=0.0.6
-    , hashable       ^>=1.4.4.0
+    , hashable       ^>=1.4.4.0 || ^>=1.5.0.0
     , QuickCheck     ^>=2.14.2  || ^>=2.15
     , some           ^>=1.0.6
     , universe-base  ^>=1.1.4
diff --git a/src/Data/Fin.hs b/src/Data/Fin.hs
--- a/src/Data/Fin.hs
+++ b/src/Data/Fin.hs
@@ -81,7 +81,7 @@
 -- >>> import qualified Data.Universe.Helpers as U
 -- >>> import Data.EqP (eqp)
 -- >>> import Data.OrdP (comparep)
--- >>> :set -XTypeApplications
+-- >>> :set -XTypeApplications -XGADTs
 
 -------------------------------------------------------------------------------
 -- Type
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
@@ -3,6 +3,7 @@
 {-# LANGUAGE EmptyCase            #-}
 {-# LANGUAGE GADTs                #-}
 {-# LANGUAGE KindSignatures       #-}
+{-# LANGUAGE PatternSynonyms      #-}
 {-# LANGUAGE RankNTypes           #-}
 {-# LANGUAGE ScopedTypeVariables  #-}
 {-# LANGUAGE StandaloneDeriving   #-}
@@ -10,6 +11,7 @@
 {-# LANGUAGE TypeFamilies         #-}
 {-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ViewPatterns         #-}
 -- | 'Nat' numbers. @DataKinds@ stuff.
 --
 -- This module re-exports "Data.Nat", and adds type-level things.
@@ -23,7 +25,7 @@
     explicitShow,
     explicitShowsPrec,
     -- * Singleton
-    SNat(..),
+    SNat(SZ,SS,SS'),
     snatToNat,
     snatToNatural,
     -- * Implicit
@@ -176,6 +178,35 @@
 snatToNatural :: forall n. SNat n -> Natural
 snatToNatural SZ = 0
 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