diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index e02f3214ea65a4f4611809c41839c59898cf53d4..d80dec80b826ce13e0d3bd59b228e34548fd88ff 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -235,9 +235,9 @@ Section channel.
   Qed.
 
   Lemma try_recv_spec {TT} c (v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
-    {{{ c ↣ <?.. x> MSG v x {{ ▷ P x }}; p x }}}
+    {{{ c ↣ <?.. x> MSG v x {{ P x }}; p x }}}
       try_recv c
-    {{{ w, RET w; (⌜w = NONEV⌝ ∗ c ↣ <?.. x> MSG v x {{ ▷ P x }}; p x) ∨
+    {{{ w, RET w; (⌜w = NONEV⌝ ∗ c ↣ <?.. x> MSG v x {{ P x }}; p x) ∨
                   (∃.. x, ⌜w = SOMEV (v x)⌝ ∗ c ↣ p x ∗ P x) }}}.
   Proof.
     assert (∀ w lp (m : TT → iMsg Σ),