exfalso - proofpattern @ ウィキ

もしも、

前提条件からFalseを導ける

ならば、

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

なぜなら、

exfalsoはforall P, False->Pを適用し、結論をFalseに変える。

前提条件からFalseを導くことで証明できる。