Stability of a formula under double negation ($\neg \neg A\to A$)

A first-order formula $A$ is stable when intuitionistic first-order logic proves $\neg \neg A\to A$. Double negations and logical falsity are stable. Logical conjunction of stable first-order formulas is stable; a logical implication is stable when its consequent is stable; and universal quantification preserves stability. For logical implication, from $\neg \neg (A\to B)$ and $A$, assuming $\neg B$ contradicts the first hypothesis, giving $\neg \neg B$ and then $B$. For universality, obtain $\neg \neg A(t)$ from $\neg \neg \forall xA(x)$ for arbitrary $t$, then use stability and generalize.