absurd - proofpattern @ ウィキ

もしも、

前提条件で0<>0のような命題が出現した

ならば、

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

なぜなら、

absurdはforall P, P->~P->Falseを適用し、Falseを導くことで命題を証明する。

absurd (0=0)を使用することでPが(0=0)となり証明できる。