小ネタです。 Abstract Rewriting Systemにおいて、「停止性と弱合流性(局所合流性)を持つ書き換え系は合流性を持つ」という定理があります*1。 この証明は、書き換え系の停止性から整礎帰納法を使って示すのが一般的です。 整礎帰納法はCoqでどうやるんだろ…