diff --git a/examples/nat.quox b/examples/nat.quox
index 3b9894a..efc834d 100644
--- a/examples/nat.quox
+++ b/examples/nat.quox
@@ -149,6 +149,8 @@ def0 times-zero : (m : ℕ) → 0 ≡ timesω m 0 : ℕ =
     succ m', ih ⇒ ih
   };
 
+{-
+-- unfinished
 def0 times-succ : (m n : ℕ) → plus m (timesω m n) ≡ timesω m (succ n) : ℕ =
   λ m n ⇒
   case m
@@ -158,5 +160,6 @@ def0 times-succ : (m n : ℕ) → plus m (timesω m n) ≡ timesω m (succ n) :
     succ m', ih ⇒
       δ 𝑖 ⇒ plus (succ n) (ih @𝑖)
   };
+-}
 
 }