I have been reading into Intuitionistic Logic, namely Heyting arithmetic, and I've bumped into this:
Corollary 3.9. Let $A_0$ be a quantifier-free formula of $\mathscr L(HA)$. Then $$HA\vdash A_0\lor\lnot A_0$$ In particular, quantifier-free formulas are provably stable, i.e. $$HA\vdash\lnot\lnot A_0\to A_0$$
Seemingly, this is a form of the LEM, but I thought this was rejected in Intuitionistic Logic? Further reading suggests that this can be shown using the fact that all prime formulas are of the form $s=t$, and thus their Godel-Gentzen translation $g(s=t)$ =$\neg\neg (s=t)$ = ($s=t$). Again, I didn't think this double negation was permitted in Intuitionistic logic?
Double negation is certainly allowed in intuitionistic logic (IL). The grammar is the same as for classical logic: they have the same well-formed formulas. But $\neg\neg p\to p$ (equivalent to LEM) is not a theorem of IL, for arbitrary formulas $p$.
The result you cite shows that for some sentences, double negation elimination does hold in IL — namely, for atomic sentences and Boolean combinations of them. Intuitively, pun intended, an atomic sentence represents a concrete fact, which we can prove or refute. A statement involving quantifiers, however, represents in IL an assertion that we can perform a certain construction, and LEM is not true of those.