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