練習問題 3.3.1

foldn Succ Zero n = n
がNatのすべての要素n，すなわち，有限数，擬数，無限数で成り立つことを証明せよ． 





n

上の帰納法を使う．




⊥の場合
   foldn Succ Zero ⊥
=  { foldn の定義．場合の枯渇 }
   ⊥

Zero の場合
   foldn Succ Zero Zero
=  { foldn の定義 }
   Zero

Succ n の場合
   foldn Succ Zero (Succ n)
=  { foldn の定義 }
   Succ (foldn Succ Zero n)
=  { 帰納法の仮定 }
   Succ n