"Потому что таков тип у той функции."

неее, плохая причина. Здесь был невидимый контекст. :) я начал писать тот ответ с "дык, сейчас я докажу просто с помощью X→¬¬X", потому что показалось, что дело в том, что нужно доказать это высказывание для X=(A | ¬A). В результате обнаружилась проблема с функцией f. А потом дошло, в чём разница и тонкость с дизъюнкцией в именно этом выражении.

N_A является доказательством того, что нельзя одновременно иметь доказательство A и ¬A. (одновременно населить типы A и A→⊥)

А M_A является доказательством того, что нельзя одновременно опровергнуть A и ¬A. (одновременно населить типы A→⊥ и (A→⊥)→⊥ - результат доказательства такой же, как и у N, т.е. M_A=N_A→⊥; разница в предпосылке)

Таким образом мы определяем исключающее "или". Вот это, по-моему, причина, почему нам нужно доказать и A→¬¬A, и (A | ¬A)→¬¬(A | ¬A) :)