From fcae19a14eeef560e1f969dd226187a848ad2ce9 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Thu, 30 Apr 2020 19:12:17 +0200
Subject: [PATCH] Made types explicit in subtyping rule

---
 theories/logrel/subtyping_rules.v | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index f08f44a..ce56588 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -262,14 +262,14 @@ Section subtyping_rules.
     iDestruct ("HAle" with "H") as "$". by iModIntro.
   Qed.
 
-  Lemma lty_le_exist_elim_l M S :
-    (∀ A, (<??> M A) <: S) -∗
-    ((<?? A> M A) <: S).
+  Lemma lty_le_exist_elim_l k (M : lty Σ k → lmsg Σ) S :
+    (∀ (A : lty Σ k), (<??> M A) <: S) -∗
+    ((<?? (A : lty Σ k)> M A) <: S).
   Proof. iIntros "#Hle !>". iApply (iProto_le_exist_elim_l_inhabited M). auto. Qed.
 
-  Lemma lty_le_exist_elim_r M S :
-    (∀ A, S <: (<!!> M A)) -∗
-    (S <: (<!! A> M A)).
+  Lemma lty_le_exist_elim_r k (M : lty Σ k → lmsg Σ) S :
+    (∀ (A : lty Σ k), S <: (<!!> M A)) -∗
+    (S <: (<!! (A : lty Σ k)> M A)).
   Proof. iIntros "#Hle !>". iApply (iProto_le_exist_elim_r_inhabited _ M). auto. Qed.
 
   Lemma lty_le_exist_intro_l k (M : lty Σ k → lmsg Σ) (A : lty Σ k) :
-- 
GitLab