<pre><code>let Y = \T. (\x. T (x x)) (\x. T (x x)) in
Y Y ≡ \T. (\x. T (x x)) (\x. T (x x)) Y
- ~~> (\x. Y (x x)) (\x. Y (x x))
- ~~> Y ((\x. Y (x x)) (\x. Y (x x)))
- ~~> Y (Y ((\x. Y (x x)) (\x. Y (x x))))
- ~~> Y (Y (Y (...(Y (Y Y))...)))</code></pre>
+~~> (\x. Y (x x)) (\x. Y (x x))
+~~> Y ((\x. Y (x x)) (\x. Y (x x)))
+~~> Y (Y ((\x. Y (x x)) (\x. Y (x x))))
+~~> Y (Y (Y (...(Y (Y Y))...)))</code></pre>
#Q: Ouch! Stop hurting my brain.#
<pre><code>let succ = \n s z. s (n s z) in
let X = (\x. succ (x x)) (\x. succ (x x)) in
succ X
- ≡ succ ( (\x. succ (x x)) (\x. succ (x x)) )
- ~~> succ (succ ( (\x. succ (x x)) (\x. succ (x x))))
- ≡ succ (succ X)</code></pre>
+≡ succ ( (\x. succ (x x)) (\x. succ (x x)) )
+~~> succ (succ ( (\x. succ (x x)) (\x. succ (x x))))
+≡ succ (succ X)</code></pre>
You should see the close similarity with `Y Y` here.