Existential quantifier in Coq impredicative logic (System F)

Question

I was trying to code into Coq logical connectives encoded in lambda calculus with type à la System F. Here is the bunch of code I wrote (standard things, I think)

Definition True := forall X : Prop, X -> X.

Lemma I : True.
True
Proof.
True
  unfold True.
forall X : Prop, X -> X intros.
X: Prop
H: X
X apply H.
Qed.

Section s.
  Variables A B : Prop.

  (* conjunction *)

  Definition and := forall X : Prop, (A -> B -> X) -> X.
  Infix "/\" := and.

  Lemma and_intro : A -> B -> A /\ B.
A, B: Prop
A -> B -> A /\ B
  Proof using A B.
A, B: Prop
A -> B -> A /\ B
    intros HA HB.
A, B: Prop
HA: A
HB: B
(A /\ B)%type split.
A, B: Prop
HA: A
HB: B
A
A, B: Prop
HA: A
HB: B
B
    -
A, B: Prop
HA: A
HB: B
A apply HA.
    -
A, B: Prop
HA: A
HB: B
B apply HB.
  Qed.

  Lemma and_elim_l : A /\ B -> A.
A, B: Prop
A /\ B -> A
  Proof using A B.
A, B: Prop
A /\ B -> A
    intros H.
A, B: Prop
H: (A /\ B)%type
A destruct H as [HA HB].
A, B: Prop
HA: A
HB: B
A apply HA.
  Qed.

  Lemma and_elim_r : A /\ B -> B.
A, B: Prop
A /\ B -> B
  Proof using A B.
A, B: Prop
A /\ B -> B
    intros H.
A, B: Prop
H: (A /\ B)%type
B destruct H as [HA HB].
A, B: Prop
HA: A
HB: B
B apply HB.
  Qed.

  (* disjunction *)

  Definition or := forall X : Prop, (A -> X) -> (B -> X) -> X.
  Infix "\/" := or.

  Lemma or_intro_l : A -> A \/ B.
A, B: Prop
A -> A \/ B
  Proof using A B.
A, B: Prop
A -> A \/ B
    intros HA.
A, B: Prop
HA: A
(A \/ B)%type left.
A, B: Prop
HA: A
A apply HA.
  Qed.

  Lemma or_elim : forall C : Prop, A \/ B -> (A -> C) -> (B -> C) -> C.
A, B: Prop
forall C : Prop, A \/ B -> (A -> C) -> (B -> C) -> C
  Proof using A B.
A, B: Prop
forall C : Prop, A \/ B -> (A -> C) -> (B -> C) -> C
    intros C HOR HAC HBC.
A, B, C: Prop
HOR: (A \/ B)%type
HAC: A -> C
HBC: B -> C
C destruct HOR.
A, B, C: Prop
H: A
HAC: A -> C
HBC: B -> C
C
A, B, C: Prop
H: B
HAC: A -> C
HBC: B -> C
C
    apply (HAC H).
A, B, C: Prop
H: B
HAC: A -> C
HBC: B -> C
C
    apply (HBC H).
  Qed.

  (* falsity *)

  Definition False := forall Y : Prop, Y.

  Lemma false_elim : False -> A.
A, B: Prop
False -> A
  Proof using A.
A, B: Prop
False -> A
    unfold False.
A, B: Prop
(forall Y : Prop, Y) -> A intros.
A, B: Prop
H: forall Y : Prop, Y
A apply (H A).
  Qed.

End s.

Basically, I wrote down the elimination and introduction laws for conjunction, disjunction, true and false. I am not sure of having done thing correctly, but I think that things should work that way. Now I would like to define the existential quantification, but I have no idea of how to proceed. Does anyone have a suggestion?

Answer

Existential quantification is just a generalization of conjunction, where the type of the second component of the pair depends on the value of the first component. When there's no dependency they're equivalent:

Goal forall P1 P2 : Prop, (exists _ : P1, P2) <-> P1 /\ P2.
forall P1 P2 : Prop, (exists _ : P1, P2) <-> P1 /\ P2
Proof.
forall P1 P2 : Prop, (exists _ : P1, P2) <-> P1 /\ P2 split; intros [H1 H2]; eauto. Qed.

Coq'Art has a section on impredicativity starting at page 130.

Inductive ex (A : Type) (P : A -> Prop) : Prop :=
    ex_intro : forall x : A, P x -> exists y, P y

Arguments ex [A]%type_scope _%function_scope
Arguments ex_intro [A]%type_scope _%function_scope _ _
Notation "'exists' x .. y , p" :=
  (ex (fun x => .. (ex (fun y => p)) ..)) : type_scope
  (default interpretation)
Notation "'exists' ! x .. y , p" :=
  (ex
     (unique
        (fun x => .. (ex (unique (fun y => p))) ..)))
  : type_scope (default interpretation)

The problem with impredicative definitions (unless I'm mistaken) is that there's no dependent elimination. It's possible prove

Goal forall (A : Type) (P : A -> Prop) (Q : Prop),
    (forall x : A, P x -> Q) -> (exists x, P x) -> Q.
forall (A : Type) (P : A -> Prop) (Q : Prop),
(forall x : A, P x -> Q) -> (exists x : A, P x) -> Q

but not

Goal forall (A : Type) (P : A -> Prop) (Q : (exists x, P x) -> Prop),
    (forall (x : A) (H : P x), Q (ex_intro P x H)) ->
    forall H : exists x, P x, Q H.
forall (A : Type) (P : A -> Prop)
  (Q : (exists x : A, P x) -> Prop),
(forall (x : A) (H : P x), Q (ex_intro P x H)) ->
forall H : exists x : A, P x, Q H