diff --git a/coq-actris.opam b/coq-actris.opam
index f60b3bdbe1423e10b62088ab2bf2b86fecd070ca..0c6a5cdb8c27e80e9dda5ed5ad68a571edae1c7a 100644
--- a/coq-actris.opam
+++ b/coq-actris.opam
@@ -8,7 +8,7 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/actris/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/iris/actris.git"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2023-05-02.4.943e9b74") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2023-05-03.3.85295b18") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 2d449a45fd8941c8efb24689209fccc82d482091..86d2ce9e566a9f1da3f7a34742109593b96ef2df 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -139,7 +139,7 @@ Section channel.
   Global Instance iProto_mapsto_proper c : Proper ((≡) ==> (≡)) (iProto_mapsto c).
   Proof. apply (ne_proper _). Qed.
 
-  Lemma iProto_mapsto_le c p1 p2 : c ↣ p1 -∗ ▷ (p1 ⊑ p2) -∗ c ↣ p2.
+  Lemma iProto_mapsto_le c p1 p2 : c ↣ p1 ⊢ ▷ (p1 ⊑ p2) -∗ c ↣ p2.
   Proof.
     rewrite iProto_mapsto_eq. iDestruct 1 as (γ s l r lk ->) "[Hlk H]".
     iIntros "Hle'". iExists γ, s, l, r, lk. iSplit; [done|]. iFrame "Hlk".
diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index 2777da8b37acf40b6cca1830fc44a342562feb2b..bcc370d0ac9f3fe5a8b7147164dfbf92ae97d481 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -209,7 +209,7 @@ Proof.
     iApply iProto_le_trans; [|iApply (iProto_le_texist_intro_r _ x)]; simpl.
     iIntros "H". by iDestruct (HP with "H") as "$". }
   rewrite -wp_bind. eapply bi.wand_apply;
-    [by eapply (recv_spec _ (tele_app tv) (tele_app tP') (tele_app tp))|f_equiv; first done].
+    [by eapply bi.wand_entails, (recv_spec _ (tele_app tv) (tele_app tP') (tele_app tp))|f_equiv; first done].
   rewrite -bi.later_intro; apply bi.forall_intro=> x.
   specialize (HΦ x). destruct (envs_app _ _) as [Δ'|] eqn:HΔ'=> //.
   rewrite envs_app_sound //; simpl. by rewrite right_id HΦ.
@@ -302,7 +302,7 @@ Proof.
     c ↣ <!.. (x : TT)> MSG tele_app tv x {{ tele_app tP x }}; tele_app tp x) as ->.
   { iIntros "Hc". iApply (iProto_mapsto_le with "Hc"); iIntros "!>".
     iApply iProto_le_trans; [iApply Hp|]. by rewrite Hm. }
-  eapply bi.wand_apply; [rewrite -wp_bind; by eapply send_spec_tele|].
+  eapply bi.wand_apply; [rewrite -wp_bind; by eapply bi.wand_entails, send_spec_tele|].
   by rewrite -bi.later_intro.
 Qed.
 
@@ -389,7 +389,7 @@ Proof.
   rewrite envs_entails_unseal /ProtoNormalize /= right_id=> ? Hp HΦ.
   rewrite envs_lookup_sound //; simpl.
   rewrite (iProto_mapsto_le _ _ (p1 <{P1}&{P2}> p2)%proto) -bi.later_intro -Hp left_id.
-  rewrite -wp_bind. eapply bi.wand_apply; [by eapply branch_spec|f_equiv; first done].
+  rewrite -wp_bind. eapply bi.wand_apply; [by eapply bi.wand_entails, branch_spec|f_equiv; first done].
   rewrite -bi.later_intro; apply bi.forall_intro=> b.
   specialize (HΦ b). destruct (envs_app _ _) as [Δ'|] eqn:HΔ'=> //.
   rewrite envs_app_sound //; simpl. by rewrite right_id HΦ.
@@ -442,7 +442,7 @@ Proof.
   rewrite envs_entails_unseal /ProtoNormalize /= right_id=> ? Hp HΦ.
   rewrite envs_lookup_sound //; simpl.
   rewrite (iProto_mapsto_le _ _ (p1 <{P1}+{P2}> p2)%proto) -bi.later_intro -Hp left_id.
-  rewrite -wp_bind. eapply bi.wand_apply; [by eapply select_spec|].
+  rewrite -wp_bind. eapply bi.wand_apply; [by eapply bi.wand_entails, select_spec|].
   rewrite -assoc; f_equiv; first done.
   destruct (envs_split _ _ _) as [[Δ1 Δ2]|] eqn:? => //.
   destruct (envs_app _ _ _) as [Δ2'|] eqn:? => //.
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index f0948044296a652f5099adc38cb25b374c56aa10..13b3a4620e34c24f4b195536fc4b8d7898e09946 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -751,7 +751,7 @@ Section proto.
   Qed.
 
   Lemma iProto_le_payload_elim_l a m v P p :
-    (P -∗ (<?> MSG v; p) ⊑ (<a> m)) -∗
+    (P -∗ (<?> MSG v; p) ⊑ (<a> m)) ⊢
     (<?> MSG v {{ P }}; p) ⊑ (<a> m).
   Proof.
     rewrite iMsg_base_eq. iIntros "H". destruct a.
@@ -761,7 +761,7 @@ Section proto.
       iApply (iProto_le_recv_recv_inv with "(H HP)"); simpl; auto.
   Qed.
   Lemma iProto_le_payload_elim_r a m v P p :
-    (P -∗ (<a> m) ⊑ (<!> MSG v; p)) -∗
+    (P -∗ (<a> m) ⊑ (<!> MSG v; p)) ⊢
     (<a> m) ⊑ (<!> MSG v {{ P }}; p).
   Proof.
     rewrite iMsg_base_eq. iIntros "H". destruct a.
@@ -786,7 +786,7 @@ Section proto.
   Qed.
 
   Lemma iProto_le_exist_elim_l {A} (m1 : A → iMsg Σ V) a m2 :
-    (∀ x, (<?> m1 x) ⊑ (<a> m2)) -∗
+    (∀ x, (<?> m1 x) ⊑ (<a> m2)) ⊢
     (<? x> m1 x) ⊑ (<a> m2).
   Proof.
     rewrite iMsg_exist_eq. iIntros "H". destruct a.
@@ -798,7 +798,7 @@ Section proto.
   Qed.
 
   Lemma iProto_le_exist_elim_l_inhabited `{!Inhabited A} (m : A → iMsg Σ V) p :
-    (∀ x, (<?> m x) ⊑ p) -∗
+    (∀ x, (<?> m x) ⊑ p) ⊢
     (<? x> m x) ⊑ p.
   Proof.
     rewrite iMsg_exist_eq. iIntros "H".
@@ -819,7 +819,7 @@ Section proto.
   Qed.
 
   Lemma iProto_le_exist_elim_r {A} a m1 (m2 : A → iMsg Σ V) :
-    (∀ x, (<a> m1) ⊑ (<!> m2 x)) -∗
+    (∀ x, (<a> m1) ⊑ (<!> m2 x)) ⊢
     (<a> m1) ⊑ (<! x> m2 x).
   Proof.
     rewrite iMsg_exist_eq. iIntros "H". destruct a.
@@ -830,7 +830,7 @@ Section proto.
       iApply (iProto_le_recv_send_inv with "H Hm1 Hm2").
   Qed.
   Lemma iProto_le_exist_elim_r_inhabited `{Hinh : Inhabited A} p (m : A → iMsg Σ V) :
-    (∀ x, p ⊑ (<!> m x)) -∗
+    (∀ x, p ⊑ (<!> m x)) ⊢
     p ⊑ (<! x> m x).
   Proof.
     rewrite iMsg_exist_eq. iIntros "H".
@@ -863,7 +863,7 @@ Section proto.
   Qed.
 
   Lemma iProto_le_texist_elim_l {TT : tele} (m1 : TT → iMsg Σ V) a m2 :
-    (∀ x, (<?> m1 x) ⊑ (<a> m2)) -∗
+    (∀ x, (<?> m1 x) ⊑ (<a> m2)) ⊢
     (<?.. x> m1 x) ⊑ (<a> m2).
   Proof.
     iIntros "H". iInduction TT as [|T TT] "IH"; simpl; [done|].
@@ -895,7 +895,7 @@ Section proto.
   Qed.
 
   Lemma iProto_le_base a v P p1 p2 :
-    ▷ (p1 ⊑ p2) -∗
+    ▷ (p1 ⊑ p2) ⊢
     (<a> MSG v {{ P }}; p1) ⊑ (<a> MSG v {{ P }}; p2).
   Proof.
     rewrite iMsg_base_eq. iIntros "H". destruct a.
@@ -948,7 +948,7 @@ Section proto.
 
   Lemma iProto_le_amber_internal (p1 p2 : iProto Σ V → iProto Σ V)
       `{Contractive p1, Contractive p2}:
-    □ (∀ rec1 rec2, ▷ (rec1 ⊑ rec2) → p1 rec1 ⊑ p2 rec2) -∗
+    □ (∀ rec1 rec2, ▷ (rec1 ⊑ rec2) → p1 rec1 ⊑ p2 rec2) ⊢
     fixpoint p1 ⊑ fixpoint p2.
   Proof.
     iIntros "#H". iLöb as "IH".
@@ -968,12 +968,12 @@ Section proto.
     - apply bi.limit_preserving_entails; [done|solve_proper].
   Qed.
 
-  Lemma iProto_le_dual_l p1 p2 : iProto_dual p2 ⊑ p1 -∗ iProto_dual p1 ⊑ p2.
+  Lemma iProto_le_dual_l p1 p2 : iProto_dual p2 ⊑ p1 ⊢ iProto_dual p1 ⊑ p2.
   Proof.
     iIntros "H". iEval (rewrite -(involutive iProto_dual p2)).
     by iApply iProto_le_dual.
   Qed.
-  Lemma iProto_le_dual_r p1 p2 : p2 ⊑ iProto_dual p1 -∗ p1 ⊑ iProto_dual p2.
+  Lemma iProto_le_dual_r p1 p2 : p2 ⊑ iProto_dual p1 ⊢ p1 ⊑ iProto_dual p2.
   Proof.
     iIntros "H". iEval (rewrite -(involutive iProto_dual p1)).
     by iApply iProto_le_dual.
diff --git a/theories/examples/swap_mapper.v b/theories/examples/swap_mapper.v
index fb6b29321cff1f23b1abff614c2b5b8bb91f337f..bc1c06edaba8695470229155b2f1e5bbdeb31709 100644
--- a/theories/examples/swap_mapper.v
+++ b/theories/examples/swap_mapper.v
@@ -62,7 +62,7 @@ Section with_Σ.
     (send_once $ recv_once $ prot).
 
   Lemma send_once_mono prot1 prot2 :
-    ▷ (∀ x, prot1 x ⊑ prot2 x) -∗ send_once prot1 ⊑ send_once prot2.
+    ▷ (∀ x, prot1 x ⊑ prot2 x) ⊢ send_once prot1 ⊑ send_once prot2.
   Proof.
     iIntros "Hsub".
     iModIntro.
@@ -76,7 +76,7 @@ Section with_Σ.
   Proof. intros _. apply send_once_mono. Qed.
 
   Lemma recv_once_mono prot1 prot2 x :
-    ▷ (prot1 ⊑ prot2) -∗ recv_once prot1 x ⊑ recv_once prot2 x.
+    ▷ (prot1 ⊑ prot2) ⊢ recv_once prot1 x ⊑ recv_once prot2 x.
   Proof.
     iIntros "Hsub".
     iIntros (w) "Hw". iExists w. iFrame "Hw". iModIntro.
@@ -89,7 +89,7 @@ Section with_Σ.
   Proof. intros _. apply recv_once_mono. Qed.
 
   Lemma map_once_mono prot1 prot2 :
-    ▷ (prot1 ⊑ prot2) -∗ map_once prot1 ⊑ map_once prot2.
+    ▷ (prot1 ⊑ prot2) ⊢ map_once prot1 ⊑ map_once prot2.
   Proof. iIntros "Hsub". iModIntro. iIntros (x). iModIntro. eauto. Qed.
 
   Global Instance map_once_from_modal p1 p2 :
diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index ef00bc478b872c4153dcb0584376b201f46bceaa..f23854abe622a94d995bb15e3b3093ee66631fb8 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -245,7 +245,7 @@ Section subtyping_rules.
   Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
 
   Lemma lty_le_chan S1 S2 :
-    ▷ (S1 <: S2) -∗ chan S1 <: chan S2.
+    ▷ (S1 <: S2) ⊢ chan S1 <: chan S2.
   Proof.
     iIntros "#Hle" (v) "!> H".
     iApply (iProto_mapsto_le with "H [Hle]"). eauto.
@@ -269,14 +269,14 @@ Section subtyping_rules.
   Qed.
 
   Lemma lty_le_exist_elim_l k (M : lty Σ k → lmsg Σ) S :
-    (∀ (A : lty Σ k), (<??> M A) <: 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 k (M : lty Σ k → lmsg Σ) S :
-    (∀ (A : lty Σ k), S <: (<!!> M A)) -∗
+    (∀ (A : lty Σ k), S <: (<!!> M A)) ⊢
     S <: (<!! (A : lty Σ k)> M A).
   Proof.
     iIntros "#Hle !>". iApply (iProto_le_exist_elim_r_inhabited _ M). auto.
@@ -291,7 +291,7 @@ Section subtyping_rules.
   Proof. iIntros "!>". iApply (iProto_le_exist_intro_r). Qed.
 
   Lemma lty_le_texist_elim_l {kt} (M : ltys Σ kt → lmsg Σ) S :
-    (∀ Xs, (<??> M Xs) <: S) -∗
+    (∀ Xs, (<??> M Xs) <: S) ⊢
     (<??.. Xs> M Xs) <: S.
   Proof.
     iIntros "H". iInduction kt as [|k kt] "IH"; simpl; [done|].
@@ -300,7 +300,7 @@ Section subtyping_rules.
   Qed.
 
   Lemma lty_le_texist_elim_r {kt : ktele Σ} (M : ltys Σ kt → lmsg Σ) S :
-    (∀ Xs, S <: (<!!> M Xs)) -∗
+    (∀ Xs, S <: (<!!> M Xs)) ⊢
     S <: (<!!.. Xs> M Xs).
   Proof.
     iIntros "H". iInduction kt as [|k kt] "IH"; simpl; [done|].
@@ -403,7 +403,7 @@ Section subtyping_rules.
   Qed.
 
   Lemma lty_le_branch (Ss1 Ss2 : gmap Z (lsty Σ)) :
-    ([∗ map] S1;S2 ∈ Ss1; Ss2, ▷ (S1 <: S2)) -∗
+    ([∗ map] S1;S2 ∈ Ss1; Ss2, ▷ (S1 <: S2)) ⊢
     lty_branch Ss1 <: lty_branch Ss2.
   Proof.
     iIntros "#H !>" (x); iDestruct 1 as %[S1 HSs1]. iExists x.