With the proviso that the non-constructive statement '∃ x such that P(x)' can also be understood constructively as '¬∀ x ¬P(x)' which does not require constructing a suitable x, so classical proofs can be modeled without adding any extra axioms to the logic. (Clearly the two statements are classically, though not constructively equivalent).

Similarly, all classical uses of LEM (A ∨ B) can be understood as constructive statements of the form ¬(¬A ∧ ¬B).