+ K(H H) == (\xy.x)((\fy.ff)(\fy.ff)
+ ~~> \y.(\fy.ff)(\fy.ff)
+
+Yep, `H H` and `K(H H)` both reduce to the same term.
+
+This fixed point is bit wierd. Let's reduce it a bit more:
+
+ H H == (\fy.ff)(\fy.ff)
+ ~~> \y.(\fy.ff)(\fy.ff)
+ ~~> \yy.(\fy.ff)(\fy.ff)
+ ~~> \yyy.(\fy.ff)(\fy.ff)
+
+It appears that where `K` is a function that ignores (only) the first
+argument you feed to it, the fixed point of `K` ignores an endless,
+infinite series of arguments. It's a write-only memory, a black hole.
+
+
+##What is a fixed point for the successor function?##
+
+As we've seen, the recipe just given for finding a fixed point worked
+great for our `h`, which we wrote as a definition for the length
+function. But the recipe doesn't make any assumptions about the
+internal structure of the function it works with. That means it can
+find a fixed point for literally any function whatsoever.
+
+In particular, what could the fixed point for the
+successor function possibly be like?