下に書いたのから、よく考えたらおかしいところを直して、option Z とかいらないじゃんとか思い直した。ここに最新のが置いてある。http://github.com/kik/sandbox/blob/master/coq/tarai.v

http://d.hatena.ne.jp/kururu_goedel/20100702これを見て、とりあえず綺麗に書き直そうとしてみたら一日かかった。 しかし、これで一般たらいまわしへの道も見えてきたかも？ここに置いた。http://github.com/kik/sandbox/blob/master/coq/tarai.v多少、解…