I need to prove that $ \neg Kp \rightarrow \neg p$ follows intuitionistically from $ p \rightarrow \neg \neg Kp$. May I ask someone to verify my proof?
In addition, I also possess a proof for $\forall p (\neg Kp \rightarrow \neg p)$ is equivalent intuitionistically to $\neg \exists p (p \wedge \neg Kp)$. The proof is a bit long so I won't post it here. May I also ask someone to verify that the two are indeed equivalent intuitionistically? Thanks very much.
If I'm reading your proof correctly, I think it is fine. That said, you can abstract from the problem greatly.
You can intuitionistically prove $(A\land B)\to C \iff A\to(B\to C)$. Often $\neg P$ is defined as $P\to\bot$ in intuitionistic logic, but it can certainly be shown to be provably equivalent to it. (You can show $\bot\iff P\land\neg P$ if you don't have $\bot$ as a connective.) Combined with $(\exists x.P(x))\to C\iff\forall x.(P(x)\to C)$ (which is secretly very closely related to the earlier equivalence), this gives you the second statement by using $A=\neg Kp$, $B=p$, and $C=\bot$ for the inner formula after applying the previous equivalence.
Of course, we can easily prove $A\land B \iff B\land A$ and thus with the above we easily have $A\to(B\to C)\iff B\to(A\to C)$. Your first statement is an example of this with $A=p$, $B=\neg Kp$, and $C=\bot$.