Added spec for telescoped version of send and bumped proofmode

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

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.