diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index c8e488654d9764b4b62889df98c9c931de720809..6e4bb0c605ddefad94832b39367f4fc3b2e3be39 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -131,7 +131,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 -∗ iProto_le p1 p2 -∗ c ↣ p2.
+  Lemma iProto_mapsto_le c p1 p2 : c ↣ p1 -∗ ▷ iProto_le 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/proto.v b/theories/channel/proto.v
index 29cd3dba11a9394228a6edccf8b3c685feb93fb0..7e62cb5eb6883301fb04d4a5603d46b208799710 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -867,7 +867,7 @@ Section proto.
   Proof. apply (ne_proper _). Qed.
 
   Lemma iProto_own_le γ s p1 p2 :
-    iProto_own γ s p1 -∗ iProto_le p1 p2 -∗ iProto_own γ s p2.
+    iProto_own γ s p1 -∗ ▷ iProto_le p1 p2 -∗ iProto_own γ s p2.
   Proof.
     iDestruct 1 as (p1') "[Hle H]". iIntros "Hle'".
     iExists p1'. iFrame "H". by iApply (iProto_le_trans with "Hle").