頭の中で証明を作る

Zorn の補題は難航中なんですが...

　　Agdaなんだから、Agda 自体が考えてくれるんじゃないの?

まぁ、細かい部分はそうなんだよな。適当に埋めて通ったり。

でも結局は、頭の中で考えてからになるみたい。

その時、その時で学びはあるわけだけど。

前順序とか半順序とかの構造が明確になるのはよいかな。

そろそろ片付いてほしいところですけどね。