Coqで”無限オブ無限”(証明部分)

ヒビルテで、さかいさんが興味深いCoqのコードを紹介していた。
⇒ λ. Coqで“無限オブ無限”
どうやら元ネタはここ(derive your dreams)らしい。

おもしろそうなので、さかいさんのコードを証明してみた。

証明した定理は以下。

Theorem main : forall m n:nat, m >= 1 -> n >= 1 ->
  Str_in (m,n) (iflatten ss).

但し、

ss =
 [[(1,1); (1,2); ...];
  [(2,1); (2,2); ...];
   :
   : ]

とする。