+##Coming at it another way##
+
+TODO
+
+
+##A fixed point for K?##
+
+Let's do one more example to illustrate. We'll do `K`, since we
+wondered above whether it had a fixed point.
+
+Before we begin, we can reason a bit about what the fixed point must
+be like. We're looking for a fixed point for `K`, i.e., `\xy.x`. The term `K`
+ignores its second argument. That means that no matter what we give
+`K` as its first argument, the result will ignore the next argument
+(that is, `KX` ignores its first argument, no matter what `X` is). So
+if `KX <~~> X`, `X` had also better ignore its first argument. But we
+also have `KX ≡ (\xy.x)X ~~> \y.X`. This means that if `X` ignores
+its first argument, then `\y.X` will ignore its first two arguments.
+So once again, if `KX <~~> X`, `X` also had better ignore (at least) its
+first two arguments. Repeating this reasoning, we realize that `X`
+must be a function that ignores as many arguments as you give it.
+Our expectation, then, is that our recipe for finding fixed points
+will build us a term that somehow manages to ignore arbitrarily many arguments.
+
+ h ≡ \xy.x
+ H ≡ \u.h(uu) ≡ \u.(\xy.x)(uu) ~~> \uy.uu
+ H H ≡ (\uy.uu)(\uy.uu) ~~> \y.(\uy.uu)(\uy.uu)
+
+Let's check that it is in fact a fixed point:
+
+ K(H H) ≡ (\xy.x)((\uy.uu)(\uy.uu)
+ ~~> \y.(\uy.uu)(\uy.uu)
+
+Yep, `H H` and `K(H H)` both reduce to the same term.
+
+To see what this fixed point does, let's reduce it a bit more:
+
+ H H ≡ (\uy.uu)(\uy.uu)
+ ~~> \y.(\uy.uu)(\uy.uu)
+ ~~> \yy.(\uy.uu)(\uy.uu)
+ ~~> \yyy.(\uy.uu)(\uy.uu)
+
+Sure enough, this fixed point ignores an endless, infinite series of
+arguments. It's a write-only memory, a black hole.
+
+Now that we have one fixed point, we can find others, for instance,
+
+ (\uy.uuu)(\uy.uuu)
+ ~~> \y.(\uy.uuu)(\uy.uuu)(\uy.uuu)
+ ~~> \yy.(\uy.uuu)(\uy.uuu)(\uy.uuu)(\uy.uuu)
+ ~~> \yyy.(\uy.uuu)(\uy.uuu)(\uy.uuu)(\uy.uuu)(\uy.uuu)
+
+Continuing in this way, you can now find an infinite number of fixed
+points, all of which have the crucial property of ignoring an infinite
+series of arguments.