diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index ba73ffb..8a8faaa 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -403,6 +403,7 @@ theorem2∙13∙1 m n = encode m n , equiv
       in what5
     backward (suc m) (suc n) c =
       let
+        IH = backward m n c
       in {!   !}
 
     equiv = record