ヒビルテで、さかいさんが興味深いCoqのコードを紹介していた。 ⇒ λ. Coqで“無限オブ無限” どうやら元ネタはここ(derive your dreams)らしい。おもしろそうなので、さかいさんのコードを証明してみた。証明した定理は以下。 Theorem main : forall m n:nat, …