diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,13 @@
 # Revision history for natural-arithmetic
 
+## 0.1.2.0 -- 2019-01-20
+
+* Add strict variant of descend.
+
+## 0.1.1.0 -- 2019-11-22
+
+* Undocumented
+
 ## 0.1.0.0 -- 2019-09-04
 
 * Initial release.
diff --git a/natural-arithmetic.cabal b/natural-arithmetic.cabal
--- a/natural-arithmetic.cabal
+++ b/natural-arithmetic.cabal
@@ -1,6 +1,6 @@
 cabal-version: 2.2
 name: natural-arithmetic
-version: 0.1.1.0
+version: 0.1.2.0
 synopsis: Arithmetic of natural numbers
 description:
   A search for terms like `arithmetic` and `natural` on hackage reveals
diff --git a/src/Arithmetic/Fin.hs b/src/Arithmetic/Fin.hs
--- a/src/Arithmetic/Fin.hs
+++ b/src/Arithmetic/Fin.hs
@@ -24,6 +24,7 @@
   , ascendM
   , ascendM_
   , descend
+  , descend'
   , descendM
   , descendM_
   , ascending
@@ -98,6 +99,26 @@
   go !m = case m <? n of
     Nothing -> b0
     Just lt -> f (Fin m lt) (go (Nat.succ m))
+
+-- | Fold over the numbers bounded by @n@ in descending
+-- order. This is strict in the accumulator. For convenince,
+-- this differs from @foldr'@ in the order of the parameters.
+--
+-- > descend 4 z f = f 0 (f 1 (f 2 (f 3 z)))
+descend' :: forall a n.
+     Nat n -- ^ Upper bound
+  -> a -- ^ Initial accumulator
+  -> (Fin n -> a -> a) -- ^ Update accumulator
+  -> a
+{-# inline descend' #-}
+descend' !n !b0 f = go n Lte.reflexive b0
+  where
+    go :: Nat p -> p <= n -> a -> a
+    go !m pLteEn !b = case Nat.monus m Nat.one of
+      Nothing -> b
+      Just (Difference (mpred :: Nat c) cPlusOneEqP) ->
+        let !cLtEn = descendLemma cPlusOneEqP pLteEn
+        in go mpred (Lte.fromStrict cLtEn) (f (Fin mpred cLtEn) b)
 
 -- | Fold over the numbers bounded by @n@ in ascending order. This
 -- is lazy in the accumulator.
diff --git a/src/Arithmetic/Types.hs b/src/Arithmetic/Types.hs
--- a/src/Arithmetic/Types.hs
+++ b/src/Arithmetic/Types.hs
@@ -23,7 +23,10 @@
 import qualified GHC.TypeNats as GHC
 
 data WithNat :: (GHC.Nat -> Type) -> Type where
-  WithNat :: Nat n -> f n -> WithNat f
+  WithNat ::
+       {-# UNPACK #-} !(Nat n)
+    -> f n
+    -> WithNat f
 
 -- | A finite set of 'n' elements. 'Fin n = { 0 .. n - 1 }'
 data Fin :: GHC.Nat -> Type where