+Let's do one more example to illustrate. We'll do `K`, since we
+wondered above whether it had a fixed point.
+
+ h := \xy.x
+ H := \f.h(ff) == \f.(\xy.x)(ff) ~~> \fy.ff
+ H H := (\fy.ff)(\fy.ff) ~~> \y.(\fy.ff)(\fy.ff)
+
+Ok, it doesn't have a normal form. But let's check that it is in fact
+a fixed point:
+
+ 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.
+