Can we prove that $\exists x \lnot F$ follows from $\lnot \forall x F$ by natural deduction using the intuitionistic rules, and RAA (reductio ad absurdum) just once?
It is usually done by using RAA twice on the assumptions $\lnot F$ and $\lnot \exists x \lnot F$. I know that $\forall x F$ doesn't follow from $\lnot \exists x \lnot F$ in intuitionistic logic, so we cannot derive $\exists x \lnot F$ from $\forall x F, \lnot \forall x F$. Moreover, if we introduced $\exists x \lnot F$ by RAA, we would have to derive $\bot$ from $\lnot \exists x \lnot F, \lnot \forall x F$; if we introduced $\exists x \lnot F$ by $\exists$-intro, we would have to derive $\lnot F$ from $\lnot \forall x F$ using RAA just once, which seems not quite likely... In both cases I don't know how to proceed.