Birdの本は手元にないので実際のところはわかりませんが，
なんだか構文的な議論と意味論的な議論がごっちゃになっていますね．

ここで定義しているNatはinfinityを値に含むので
無限リストのように無限的なものです．

このようなものは帰納的にではなく余帰納的に定義されているとみなし，
構文的に証明するには帰納法ではなく余帰納法を使います．
この場合は帰納法のような最初の仮定はありません．
その代わりにNat上の同値関係=が
最大の双模倣であることを証明しなければなりません．
上にはこの部分の証明がありません．

また一方で意味論的に証明するにはモデルとその完全性が必要ですが，
そのときにそもそもm+infinity=mが成り立つように定義するので
上のような構文的な証明のステップを踏む必要は特にありません．

たぶん著者は直観的な理解をしてもらうことを優先したのでしょうけど
厳密な証明としてはおかしくなっているように読めます．
どちらにしてもちゃんとした説明はちょっと長くなりますね．