2 + 2 = 4 の証明、ナイーブにプロトタイピングしたら、なんだかとても滑稽な感じになってしまった・・・、

theorem 2 + 2 = 4 {
  4 = S(3)
  3 = S(2)
  4 = S(S(2))
  2 = S(1)
  4 = S(S(S(1)))
  1 = S(0)
  4 = S(S(S(S(0))))
  2 + 2 = 2 + S(1)
  2 + 2 = S(2 + 1)
  2 + 1 = 2 + S(0)
  2 + 1 = S(2 + 0)
  2 + 0 = 2
  2 + 2 = S(S(2 + 0))
  2 + 2 = S(S(2))
  2 + 2 = S(S(S(1)))
  2 + 2 = S(S(S(S(0))))
  2 + 2 = 4
  QED
}