「inversion」の編集履歴（バックアップ）一覧はこちら

「inversion」(2014/08/09 (土) 19:13:59) の最新版変更点

追加された行は緑色になります。

削除された行は赤色になります。

もしも、

前提条件に(S O = O)のような、
明らかに異なる値の等式がある

ならば、

タクティック [[inversion>http://coq.inria.fr/distrib/current/refman/Reference-Manual010.html#hevea_tactic87]] を適用する。

なぜなら、

inversionは異なるコンストラクタの等式から矛盾を導く。
// 本当？