Assume we have a proof term of the form $(a^{A\rightarrow^c B\rightarrow^{nc} C}b^Ac^B)^C$, where $c$ is classical (that is, contains free instances of duplex negatio affirmat). The extracted term would not depend on $c$ anymore, so in fact, from a pragmatic point of view, one could accept this proof as "constructive" in the sense that the computational content of it is constructive, and only additional assertions (which are not computationally relevant) and which hence do only have to be "true", but not "constructive", are non-constructive.
My question now is, to what extent the system becomes stronger, when allowing this. Of course, it is trivial to give examples where this method is stronger, for example, as $B$ is arbitrary, we can just set $B$ to something that is only classically provable. But I did not find any example where this strengthening is relevant for the algorithm to work, that is, where it actually makes sense to allow classical reasoning, and the additional assertion $B$ cannot just be dropped.
Edit: $\rightarrow^c$ and $\rightarrow^{nc}$ mean computational ad non-computational implication, respectively. That is, the type $\tau(A\rightarrow^c B)=\tau(A)\rightarrow\tau(B)$, while $\tau(A\rightarrow^{nc}B)=\tau(B)$. In http://www.mathematik.uni-muenchen.de/~schwicht/slides/reykjavik08.pdf there can be found a definition of this, they write $\rightarrow^U$ for $\rightarrow^{nc}$. I hope this clears up the notation.
Edit 2: To make it clearer: Assume I have a list-sorting algorithm $sort_R^{\forall_{l^{L_\alpha}} (\forall_{a^\alpha}\forall_{b^\alpha}. Rab\vee\lnot Rab)\rightarrow^c \forall_{a^\alpha} Raa \rightarrow^{nc} (\forall_{a^\alpha,b^\alpha,c^\alpha}. Rab\rightarrow^{nc}Rbc\rightarrow^{nc}Rac)\rightarrow^{nc}\exists_{m^{L_\alpha}}.X(m,l)}$ where $X(m,l)$ shall stand for $m$ being sorted with respect to $R$ and containing the same elements as $l$ (It would not become clearer if I wrote that part out). The type signature sais that it needs a function deciding whether $Rab$ holds for $a$ and $b$, but it does not need a realizer of $\forall_a Raa$, nor does it need a realizer of transitivity - it just needs to know that $R$ is reflexive and transitive, but the parts where this is proved will never be called in the extracted term. So in theory, we could as well allow that these are proven classically rather than intuitionistically, since we do not need any realizers. Even worse, we might allow them to use some strong version of Choice, as long as we "believe" choice. My question is whether somebody can give an example where this is actually relevant. I tried to construct one using the given example, but I failed so far.
