Signed-off-by: Jim Pryor <profjim@jimpryor.net>
`T` has a fixed point, then there exists some `X` such that `X <~~>
TX` (that's what it means to *have* a fixed point).
`T` has a fixed point, then there exists some `X` such that `X <~~>
TX` (that's what it means to *have* a fixed point).
-<pre>
-let W = \x.T(xx) in
-let X = WW in
-X = WW = (\x.T(xx))W = T(WW) = TX
-</pre>
+<pre><code>
+let L = \x. T (x x) in
+let X = L L in
+X ≡ L L ≡ (\x. T (x x)) L ~~> T (L L) ≡ T X
+</code></pre>
Please slow down and make sure that you understand what justified each
of the equalities in the last line.
Please slow down and make sure that you understand what justified each
of the equalities in the last line.