  In a recent paper, Herbelin developed a calculus dPA$^\omega$ in which
constructive proofs for the axioms of countable and dependent choices could be
derived via the encoding of a proof of countable universal quantification as a
stream of it components. However, the property of normalization (and therefore
the one of soundness) was only conjectured. The difficulty for the proof of
normalization is due to the simultaneous presence of dependent dependent types
(for the constructive part of the choice), of control operators (for classical
logic), of coinductive objects (to encode functions of type $N\rightarrow A$
into streams $(a_0,a_1,\ldots)$) and of lazy evaluation with sharing (for these
coinductive objects).Building on previous works, we introduce in this paper a
variant of dPA$^\omega$ presented as a sequent calculus. On the one hand, we
take advantage of a variant of Krivine classical realizability we developed to
prove the normalization of classical call-by-need. On the other hand, we
benefit of dL, a classical sequent calculus with dependent types in which type
safety is ensured using delimited continuations together with a syntactic
restriction. By combining the techniques developed in these papers, we manage
to define a realizability interpretation {\`a} la Krivine of our calculus that
allows us to prove normalization and soundness.
