inversion - proofpattern @ ウィキ

もしも、

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

ならば、

タクティック inversion を適用する。

なぜなら、

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