再帰型が登場すると strong normalization が破綻する、normalization の中身読んでないので空気を読むと、型がついてても発散する項がありえるって話に驚き。あと D = μX.X→X（= D→D）と言う型で型無しラムダ計算を埋め込めてしまう……。無限はヤバイ。
Iso-recursive アプローチに登場する unfold [T] は recursive type を1段階展開する。fold [T] はその逆。実装が面倒そうなのだけど、この型をもった項を「作る」ときと「使う」ときにそれぞれ fold, unfold が対応するので、実際には破滅的に難しいというわけではなさそうだ。（p. 278）
Metatheory はスキップするつもりだけど、むしろここがおもしろそうなので 16, 21 章は後で読む。
