diff --git a/opam b/opam
index b0c9568551efe4a1c8468e34e78e4f09d269e279..048f1379046e58c3a331257c12dbc5d8bddc611e 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
 depends: [
-  "coq-iris" { (= "dev.2020-06-18.3.5f98a0bf") | (= "dev") }
+  "coq-iris" { (= "dev.2020-07-21.2.e989ad6b") | (= "dev") }
 ]
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index f6b965f03ef71f7e25fb25f50a6fccc32aaa725d..fe123a17589254c4a4e4c67a6defc7dec4b78104 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -1234,12 +1234,16 @@ Section proto.
 
   (** The instances below make it possible to use the tactics [iIntros],
   [iExist], [iSplitL]/[iSplitR], [iFrame] and [iModIntro] on [iProto_le] goals. *)
-  Global Instance iProto_le_from_forall_l {A} a (m1 : A → iMsg Σ V) m2 :
-    FromForall ((<? x> m1 x) ⊑ (<a> m2)) (λ x, (<?> m1 x) ⊑ (<a> m2))%I | 10.
-  Proof. apply iProto_le_exist_elim_l. Qed.
-  Global Instance iProto_le_from_forall_r {A} a m1 (m2 : A → iMsg Σ V) :
-    FromForall ((<a> m1) ⊑ (<! x> m2 x)) (λ x, (<a> m1) ⊑ (<!> m2 x))%I | 11.
-  Proof. apply iProto_le_exist_elim_r. Qed.
+  Global Instance iProto_le_from_forall_l {A} a (m1 : A → iMsg Σ V) m2 name :
+    AsIdentName m1 name →
+    FromForall (iProto_message Recv (iMsg_exist m1) ⊑ (<a> m2))
+               (λ x, (<?> m1 x) ⊑ (<a> m2))%I name | 10.
+  Proof. intros _. apply iProto_le_exist_elim_l. Qed.
+  Global Instance iProto_le_from_forall_r {A} a m1 (m2 : A → iMsg Σ V) name :
+    AsIdentName m2 name →
+    FromForall ((<a> m1) ⊑ iProto_message Send (iMsg_exist m2))
+               (λ x, (<a> m1) ⊑ (<!> m2 x))%I name | 11.
+  Proof. intros _. apply iProto_le_exist_elim_r. Qed.
 
   Global Instance iProto_le_from_wand_l a m v P p :
     TCIf (TCEq P True%I) False TCTrue →
diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index d27f1875f3b1a6980b3dc7862807e9d9ebdf27ae..0b704493d8c8b3a934848ad4c0f966f8417c068d 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -497,12 +497,14 @@ Section subtyping_rules.
   [iExist], [iSplitL]/[iSplitR], [iFrame] and [iModIntro] on [lty_le] goals.
   These instances have higher precedence than the ones in [proto.v] to avoid
   needless unfolding of the subtyping relation. *)
-  Global Instance lty_le_from_forall_l k (M : lty Σ k → lmsg Σ) (S : lsty Σ) :
-    FromForall ((<?? X> M X) <: S) (λ X, (<??> M X) <: S)%I | 0.
-  Proof. apply lty_le_exist_elim_l. Qed.
-  Global Instance lty_le_from_forall_r k (S : lsty Σ) (M : lty Σ k → lmsg Σ) :
-    FromForall (S <: (<!! X> M X)) (λ X, S <: (<!!> M X))%I | 1.
-  Proof. apply lty_le_exist_elim_r. Qed.
+  Global Instance lty_le_from_forall_l k (M : lty Σ k → lmsg Σ) (S : lsty Σ) name :
+    AsIdentName M name →
+    FromForall (lty_message Recv (lty_msg_exist M) <: S) (λ X, (<??> M X) <: S)%I name | 0.
+  Proof. intros _. apply lty_le_exist_elim_l. Qed.
+  Global Instance lty_le_from_forall_r k (S : lsty Σ) (M : lty Σ k → lmsg Σ) name :
+    AsIdentName M name →
+    FromForall (S <: lty_message Send (lty_msg_exist M)) (λ X, S <: (<!!> M X))%I name | 1.
+  Proof. intros _. apply lty_le_exist_elim_r. Qed.
 
   Global Instance lty_le_from_exist_l k (M : lty Σ k → lmsg Σ) S :
     FromExist ((<!! X> M X) <: S) (λ X, (<!!> M X) <: S)%I | 0.