One conservative extension of formal mathematic analysis with a scheme of dependent choice - Levin, A. M. (Springer, 1977)
http://dx.doi.org/10.1007/BF01147693
Keywords: SA-SP