3 ms·

proof : ¬¬¬¬ϕ ⇒ ¬¬ϕ proof (f : ((((a -> False) -> False) -> False) -> False)) = \ (z : a -> False) -> f (\afff -> afff (\aff -> aff z)))