хм, вообще-то не очень понятно, почему доказывается именно ¬¬(A | ¬A). Потому что на самом деле доказательство перефразирует A→¬¬A (т.е. если A доказуемо, то ¬¬A доказуемо):

N : A→((A→⊥)→⊥)
N = flip id


А теперь концептуальный такой вопрос.

Как можно в принципе написать функцию f : (Either A (A → ⊥)) → ⊥ ? Она же не может быть тотальной. То есть, будет ли доказательством (Either A (A → ⊥)) → ⊥ функция, которая матчит только Left или только Right?

Если да, то не очень ясно, каким боком это доказательство (нутро требует доказательство ∀ x:(Either A (A → ⊥)), а не ∃).

Если нет, то не ясно, как можно вообще написать функцию, которая делает и (Left x) → ⊥, и (Right f) → ⊥