AG(食べ放題 → AX 食べ過ぎ) が偽に。しばらく Coq をいじっていたせいで ¬¬P を機械的に P とするのに少し違和感を覚えるようになったが、(P→Q)→(¬P∨Q) は全然ウェルカム。まったく自分のセンスなんぞそんなもんである。

大学の池のまわりがちょっとしたハイキングコースになっていることを、4 年目にして初めて知った。今日は暖かくて、歩くにはとても良い気候。