From d809751b5ce1d14a549d10c1bebc5199ab229a19 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Dani=C3=ABl=20Louwrink?= <daniel.louwrink@gmail.com>
Date: Fri, 1 May 2020 21:55:29 +0200
Subject: [PATCH] remove bounded quantification

---
 theories/logrel/subtyping_rules.v | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index f9f315a..ef945aa 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -186,12 +186,13 @@ Section subtyping_rules.
     iSplit; iIntros "!>" (v); iDestruct 1 as (A) "#Hv";
       iExists A; repeat iModIntro; iApply "Hv".
   Qed.
-  Lemma lty_copyable_exist {k} (Mlow Mup : lty Σ k) C :
-    ▷ (∀ M, Mlow <: M -∗ M <: Mup -∗ lty_copyable (C M)) -∗ lty_copyable (lty_exist Mlow Mup C).
+
+  Lemma lty_copyable_exist (C : ltty Σ → ltty Σ) :
+    ▷ (∀ M, lty_copyable (C M)) -∗ lty_copyable (lty_exist C).
   Proof.
     iIntros "#Hle". rewrite /lty_copyable /tc_opaque.
     iApply lty_le_r; last by iApply lty_le_exist_copy.
-    iApply lty_le_exist; try (iAssumption || iApply lty_le_refl).
+    iApply lty_le_exist. iApply "Hle".
   Qed.
 
   (* TODO: Try to add Löb induction in the type system, and use it to prove μX.int → X <:> μX.int → int → X *)
-- 
GitLab