対偶の導入
$ A \to B \models \lnot B \to \lnot A
#ない言葉
直観主義論理でも成り立つ
#対偶
#対偶の除去