diff --git a/Data/Natural/Class.hs b/Data/Natural/Class.hs
--- a/Data/Natural/Class.hs
+++ b/Data/Natural/Class.hs
@@ -1,5 +1,6 @@
 module Data.Natural.Class where
 
+import Prelude hiding (iterate)
 import Data.Functor.Const
 import Data.Peano
 import Data.Proxy
@@ -13,6 +14,9 @@
 instance Natural n => Natural (Succ n) where
     natural _ sf = sf
 
-reify :: Natural n => Proxy n -> Peano
-reify (Proxy :: Proxy n) = getConst $ natural @n (Const Zero) (φ $ Const . Succ . reify)
-  where φ = ($ Proxy) :: ∀ f a . (Proxy a -> f a) -> f a
+reify :: Natural n => Const Peano n
+reify = iterate Succ Zero
+
+iterate :: ∀ n a . Natural n => (a -> a) -> a -> Const a n
+iterate f a = natural (Const a) (f' (iterate f a))
+  where f' = Const . f . getConst :: ∀ n . Const a n -> Const a (Succ n)
diff --git a/natural-induction.cabal b/natural-induction.cabal
--- a/natural-induction.cabal
+++ b/natural-induction.cabal
@@ -1,5 +1,5 @@
 name:                natural-induction
-version:             0.1.1.0
+version:             0.2.0.0
 synopsis:            Induction over natural numbers
 -- description:         
 license:             BSD3