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?