A Constructive Proof of Dependent Choice, Compatible with Classical Logic
—————————————————————————————————————————————————————————————————————————
                                (ERRATA)

Section III.A:

The type of "nth_C n" is "R_C(0) → A(n)", instead of "R_C(0) → R_C(n)".

Section III.C:

The weaker form of BI that can be obtained intuitionistically from
BI_c is

  ∀f ∃n B(f|n)
  → ∀g [∀l (B(l) → g(l)=0) ∧ ∀l (g(l)≠0 → ∃x g(l⋆x)≠0)] → g(〈〉)=0

To get

  ∀f ∃n B(f|n)
  → ∀g [∀l (B(l) → g(l)=0) ∧ ∀l (∀x g(l⋆x)=0 → g(l)=0)] → g(〈〉)=0

as indicated, Markov's principle is needed.