X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week4.mdwn;h=78e2d37e8a4363b6ebe10e46baa2e0205148ab08;hp=5238b261998d66a0651120cd0c27ed9315d33c6b;hb=21d0ff6296bd67c8828a6968b9e909078aa3aa67;hpb=7d59a94d25530ed5d0bbb53f97af3bff3bc6a532;ds=sidebyside

diff --git a/week4.mdwn b/week4.mdwn
index 5238b261..78e2d37e 100644
--- a/week4.mdwn
+++ b/week4.mdwn
@@ -69,9 +69,9 @@ succ X
 ≡ (\n s z. s (n s z)) X 
 ~~> \s z. s (X s z)
 <~~> succ (\s z. s (X s z)) ; using fixed-point reasoning
-~~> \s z. s ([succ (\s z. s (X s z))] s z)
-~~> \s z. s ([\s z. s ([succ (\s z. s (X s z))] s z)] s z)
-~~> \s z. s (s (succ (\s z. s (X s z))))
+&equiv; (\n s z. s (n s z)) (\s z. s (X s z))
+~~> \s z. s ((\s z. s (X s z)) s z)
+~~> \s z. s (s (X s z))
 </code></pre>
 
 So `succ X` looks like a numeral: it takes two arguments, `s` and `z`,