logic - coq の非予測的論理 (システム F) の存在量指定子

Question

私はラムダ計算でコード化された Coq 論理結合子をシステム F の型でコーディングしようとしていました。これが私が書いたコードの束です (標準的なものだと思います)。

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

Lemma I: True.
Proof.
  unfold True. intros. 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.
Proof.
  intros HA HB. split.
  apply HA.
  apply HB.
Qed.

Lemma and_elim_l: A/\B -> A.
Proof.
  intros H. destruct H as [HA HB]. apply HA.
Qed.

Lemma and_elim_r: A/\B -> B.
Proof.
  intros H. destruct H as [HA HB]. apply HB.
Qed.



(* disjunction *)

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

Lemma or_intro_l: A -> A\/B.
  intros HA. left. apply HA.
Qed.

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


(* falsity *)

Definition False := forall Y:Prop, Y.

Lemma false_elim: False -> A.
Proof.
  unfold False. intros. apply (H A).
Qed.

End s.

基本的には、接続詞、選言、真偽の消去法と導入法を書き留めました。私は物事が正しく行われたかどうか確信が持てませんが、物事はそのように機能するはずだと思います。今、私は存在量化を定義したいと思っていますが、どのように進めればよいかわかりません。誰か提案がありますか？