Is it possible to show $(\lnot p \implies p) \implies p \vdash (\lnot \lnot p \implies p)$ in constructive logic? I was given the task of showing that $(\lnot p \implies p)  \vdash p$ cannot be proven in constructive logic (that is, a system with no excluded middle, double negation, or $\lnot$-elimination).
I'm trying to assume that a proof for it exists and use that to show the law of excluded middle, or double negation to arrive at a contradiction. However, I'm a bit stuck and I'm not sure if this is the right approach.
Any input appreciated!
 A: $\def\fitch#1#2{~~\begin{array}{|l}#1\\\hline#2\end{array}}\fitch{(\neg p\to p)\to p}{\fitch{\neg\neg p}{\fitch{\neg p}{\bot\\p}\\\neg p\to p\\p}\\\neg\neg p\to p}$
Take $(\neg p\to p)\to p$ as a premise.  Assume $\neg\neg p$ and $\neg p$.  Derive $p$ by explosion of the contradiction (EFQ). Deduce $\neg p\to p$ by discharging the second assumption (ie $\to$-introduction). Derive $p$ by modus ponens with the premise (or $\to$-elimination). Deduce $\neg\neg p\to p$ by discharging the first premise ($\to$-introduction).
This demonstrates that $(\neg p\to p)\to p\vdash \neg\neg p\to p$ may be derived using only rules of inference acceptable in constructive logic .
Therefore $(\neg\ p\to p)\to p$ can not be a theorem in constructive logic since it constructively entails $\neg\neg p\to p$, which is definitely not a theorem in constructive logic,
A: Yes. We can reduce as $$(\lnot p\to p)\to p,\lnot\lnot p\vdash p,$$ and then it suffices to show $$ (\lnot p\to p)\to p, \lnot\lnot p\vdash \lnot p \to p,$$ and again we can reduce that to $$ (\lnot p\to p)\to p,\lnot\lnot p, \lnot p\vdash p,$$ and we see we have a statement and its negation to the left of the turnstyle and we're done.
Observe that the left-hand side of the turnstyle in your title has the schematic form of proof by contradiction (note, nothing would change with the above proof if we replaced with $(\lnot p \to \bot)\to p$, and indeed this does not change the semantics of the statement, since we can prove $\bot$ from $\lnot p$ if and only if we can prove $p$ from $\lnot p$). Thus, we might expect this to be an equivalence. And it is... try to prove the other direction.
