Library AD

Theorem AD M : (∀ x, M x ∨ ¬ M x) → lacc M → lacc (complement M) → ldec M.