More than 1 year has passed since last update.

遅れましたすみません。

ということで、前回の続きみたいなものである

Setoid の Proper な Map を作る。
http://mathink.net/program/coq_map.html

です。前回の記事を読んでいなくても大体読めますが、コードを動かすには前回のコードも必要です。