[proofplan] Unfold the sigma-one hypothesis by choosing a decidable predicate $R: \mathbb{N} \to \operatorname{Prop}$ whose existential statement is equivalent to $A$. Starting from $\neg\neg A$, we transport double negation across this equivalence to obtain $\neg\neg(\exists n \in \mathbb{N}, R(n))$. Markov's principle applies to the decidable predicate $R$, producing a witness $n$ with $R(n)$, and the equivalence then transports this existential witness back to $A$. [/proofplan] [step:Choose a decidable predicate representing the sigma-one proposition] Since $A$ is sigma-one, there exists a decidable predicate $R: \mathbb{N} \to \operatorname{Prop}$ such that \begin{align*} A \iff \exists n \in \mathbb{N}, R(n). \end{align*} Fix such a predicate $R$. Write $E$ for the proposition $\exists n \in \mathbb{N}, R(n)$. Thus we have implications \begin{align*} \alpha: A \to E \end{align*} and \begin{align*} \beta: E \to A. \end{align*} [/step] [step:Transport double negation from $A$ to the existential statement] Assume $h: \neg\neg A$. We prove $\neg\neg E$. Let $k: \neg E$ be arbitrary. Define $\ell: \neg A$ by \begin{align*} \ell(a) = k(\alpha(a)) \end{align*} for $a: A$. Since $h$ has type $\neg\neg A$, applying $h$ to $\ell$ gives a contradiction. Therefore no such $k$ can exist, and hence $\neg\neg E$ holds. [guided] Assume $h: \neg\neg A$. The goal is not yet to prove $A$ directly; Markov's principle applies only to an existential statement over a decidable predicate. Therefore we first convert $h$ into a proof of double negation for the proposition \begin{align*} E := \exists n \in \mathbb{N}, R(n). \end{align*} To prove $\neg\neg E$, let $k: \neg E$ be arbitrary. We must derive a contradiction. The equivalence between $A$ and $E$ gives the implication \begin{align*} \alpha: A \to E. \end{align*} Using $k$ and $\alpha$, define a negation of $A$ as follows: for any $a: A$, \begin{align*} \ell(a) = k(\alpha(a)). \end{align*} This is well-typed because $\alpha(a): E$, and $k$ maps any proof of $E$ to a contradiction. Hence $\ell: \neg A$. Now $h: \neg\neg A$ says precisely that every proof of $\neg A$ leads to contradiction. Applying $h$ to $\ell$ gives a contradiction. Since the assumed $k: \neg E$ was arbitrary, this proves \begin{align*} \neg\neg E. \end{align*} [/guided] [/step] [step:Apply Markov's principle and return to $A$] The predicate $R: \mathbb{N} \to \operatorname{Prop}$ is decidable by the sigma-one representation of $A$. By Markov's principle applied to $R$, the proof of $\neg\neg E$ obtained above yields a proof of \begin{align*} E = \exists n \in \mathbb{N}, R(n). \end{align*} Applying $\beta: E \to A$ to this existential proof gives $A$. Therefore $\neg\neg A \to A$. [/step]