1ère version rédigée en janvier 2011. Nombreuses corrections, et raffinements, appliqués après coup.
A Constructive Proof of Dependent Choice, Compatible with Classical Logic