そう、だから
P を仮定
¬P⇒¬P
⇒¬P∨¬¬P
だから直観論理でも⇒¬P∨¬¬P
は使える。なので直観主義で場合分けするなら
¬Pと¬¬Pに場合分けする証明ならわかるけど
Pと¬¬Pに場合分けするならそれは古典論理でしかない。
しかしそもそも古典論理なら¬¬¬P⇒¬Pの形に制限する意味がない
後付けの解説文がおかしい