diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 0832aa2efce8cbbe890464798b3365b893b8c582..6a69f5ecd646203501019e976be72dd61126daef 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -239,6 +239,22 @@ Section channel.
       iIntros "_". iApply "HΦ". iExists γ, Right, l, r, lk. eauto 10 with iFrame.
   Qed.
 
+  Lemma send_spec_tele {TT} c (tt : TT)
+        (v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
+    {{{ c ↣ (<!.. x > MSG v x {{ P x }}; p x) ∗ P tt }}}
+      send c (v tt)
+    {{{ RET #(); c ↣ (p tt) }}}.
+  Proof.
+    iIntros (Φ) "[Hc HP] HΦ".
+    iDestruct (iProto_mapsto_le _ _ (<!> MSG v tt; p tt)%proto with "Hc [HP]")
+      as "Hc".
+    { iIntros "!>".
+      iApply iProto_le_trans.
+      iApply iProto_le_texist_intro_l.
+      by iFrame "HP". }
+    by iApply (send_spec with "Hc").
+  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 }}}
       try_recv c
diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index 58701fb4fe75286f990a7d56b976900a5118c676..24b5683ce3d81682a8a70901d3ffce8ce70c12a8 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -312,12 +312,11 @@ Proof.
   destruct (envs_app _ _ _) as [Δ2'|] eqn:? => //.
   rewrite envs_split_sound //; rewrite (envs_app_sound Δ2) //; simpl.
   destruct HΦ as (-> & -> & ->). rewrite right_id assoc.
-  assert (c ↣ p ∗ tele_app tP x ⊢
-    c ↣ <!> MSG tele_app tv x; tele_app tp x) as ->.
-  { iIntros "[Hc Hm]". iApply (iProto_mapsto_le with "Hc"); iIntros "!>".
-    iApply iProto_le_trans; [iApply Hp|]. rewrite Hm.
-    iApply iProto_le_trans; [iApply iProto_le_texist_intro_l|]. by iFrame. }
-  eapply bi.wand_apply; [rewrite -wp_bind; by eapply send_spec|].
+  assert (c ↣ p ⊢
+    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|].
   by rewrite -bi.later_intro.
 Qed.