From 8453ed18a52bd7bf80be5f78fba5f106234a5755 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Fri, 17 Apr 2020 13:01:04 +0200
Subject: [PATCH] Added existential quantification elimination rule

---
 theories/logrel/subtyping.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index f864d2e..2dc0f77 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -99,6 +99,10 @@ Section subtype.
     iIntros "#Hle" (v) "!>". iDestruct 1 as (A) "H". iExists A. by iApply "Hle".
   Qed.
 
+  Lemma lty_exist_le_elim C B :
+    ⊢ (C B) <: (∃ A, C A).
+  Proof. iIntros "!>" (v) "Hle". by iExists B. Qed.
+
   Lemma lty_rec_le_1 (C : lty Σ → lty Σ) `{!Contractive C} :
     ⊢ lty_rec C <: C (lty_rec C).
   Proof.
-- 
GitLab