Is this relationship between forall and is provable in Coq / intuitionistic logic?

Question

Is the following theorem proved in Coq? And if not, is there a way to prove that this is not provable?

Theorem not_for_all_is_exists:
    forall (X : Set) (P : X -> Prop), ~(forall x : X, ~ P x) -> (exists x: X, P x).

I know this relation is true:

Theorem forall_is_not_exists : (forall (X : Set) (P : X -> Prop), (forall x, ~(P x)) -> ~(exists x, P x)).
Proof.
  (* This could probably be shortened, but I'm just starting out. *)
  intros X P.
  intros forall_x_not_Px.
  unfold not.
  intros exists_x_Px.
  destruct exists_x_Px as [ witness proof_of_Pwitness].
  pose (not_Pwitness := forall_x_not_Px witness).
  unfold not in not_Pwitness.
  pose (proof_of_False := not_Pwitness proof_of_Pwitness).
  case proof_of_False.
Qed.

But I'm not sure what helps me without double negative elimination. I also played with the proof of the theorem in question, with different approaches, but to no avail. I'm just learning Coq, so maybe I just missed something obvious.

NB I know well that this is true in classical logic, so I am not looking for evidence that adds additional axioms to the base system.

Answer 1

, ( ).

Coq , , .

X unit P fun _ => X X : Prop. ~(unit -> ~ X) -> exists (u : unit), X. - unit ~ ~ X -> X.

~ ~ (exists x, P x).

Agda , ( , , ):

open import Relation.Nullary
open import Data.Product
open import Data.Unit
open import Data.Empty
open import Function

∀∃ : Set _
∀∃ = (A : Set)(P : A → Set) → ¬ (∀ x → ¬ P x) → ∃ P

Dneg : Set _
Dneg = (A : Set) → ¬ ¬ A → A

to : ∀∃ → Dneg
to ∀∃ A ¬¬A = proj₂ (∀∃ ⊤ (const A) (λ f → ¬¬A (f tt)))

fro : Dneg → ∀∃
fro dneg A P f = dneg (∃ P) (f ∘ curry)

Answer 2

not_for_all_is_exists Coq. " " 5. .

( , Coq), exists x, P x, ( ), x, P x.

, not (forall x, not (P x)) , " , P x, ", , , P.

, Coq P x, - P x .