Is $\neg \neg \forall \neg \neg A \leftrightarrow \forall \neg \neg A$ intuitionistic derviable? Is the following a rule which is derivable in intuitionistic logic:
$\neg \neg \forall \neg \neg A \leftrightarrow \forall \neg \neg A$
I thought that I read it somewhere,... hope that someone can help me.
Thank you in advance.

The right to left is trivial, because $p \to \lnot \lnot p$ holds intuitionistically.
For the left to right:
1) $\lnot \lnot \forall x \lnot \lnot A$ --- premise
2) $\lnot A$ --- assumed [a]
3) $\forall x \lnot \lnot A$ --- assumed [b]
4) $\lnot \lnot A$ --- from 3) by $\forall$-elim
5) $\bot$ --- from 2) and 4) by $\to$-elim
6) $\lnot \forall x \lnot \lnot A$ --- from 3) by $\to$-intro, discharging [b]
7) $\bot$ --- from 1) and 6) by $\to$-elim
8) $\lnot \lnot A$ --- from 2) and 7) by $\to$-intro, discharging [a]

9) $\forall x \lnot \lnot A$ --- from 8) by $\forall$-intro.

