Simplified recv_spec

multi_actris/channel/channel.v

@@ -422,8 +422,8 @@ Section channel.
     by iApply (send_spec with "Hc").
   Qed.
 
-  Lemma recv_spec {TT} c j (v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
-    {{{ c ↣ <(Recv, j) @.. x> MSG v x {{ ▷ P x }}; p x }}}
+  Lemma recv_spec {A} c j (v : A → val) (P : A → iProp Σ) (p : A → iProto Σ) :
+    {{{ c ↣ <(Recv, j) @ x> MSG v x {{ ▷ P x }}; p x }}}
       recv c #j
     {{{ x, RET v x; c ↣ p x ∗ P x }}}.
   Proof.
@@ -473,8 +473,8 @@ Section channel.
     iSplitL "Hl' Hown Hp'".
     { iRight. iRight. iExists _. iFrame. }
     wp_pure _.
-    rewrite iMsg_base_eq.
-    iDestruct (iMsg_texist_exist with "Hm") as (x <-) "[Hp HP]".
+    rewrite iMsg_base_eq iMsg_exist_eq.
+    iDestruct "Hm" as (x <-) "[Hp HP]".
     wp_pures.
     iMod (own_update_2 with "H● H◯") as "[H● H◯]";[apply excl_auth_update|].
     iModIntro. iApply "HΦ".

multi_actris/channel/proofmode.v

@@ -170,13 +170,12 @@ Proof.
   rewrite envs_entails_unseal /ProtoNormalize /MsgTele /MaybeIntoLaterN /=.
   rewrite !tforall_forall right_id.
   intros ? Hp Hm HP HΦ. rewrite envs_lookup_sound //; simpl.
-  assert (c ↣ p ⊢ c ↣ <(Recv,n) @.. x>
+  assert (c ↣ p ⊢ c ↣ <(Recv,n) @ x>
     MSG tele_app tv x {{ ▷ tele_app tP' x }}; tele_app tp x) as ->.
   { iIntros "Hc". iApply (iProto_pointsto_le with "Hc"). iIntros "!>".
     iApply iProto_le_trans; [iApply Hp|rewrite Hm].
     iApply iProto_le_texist_elim_l; iIntros (x).
-    iApply iProto_le_trans; [|iApply (iProto_le_texist_intro_r _ _ x)]; simpl.
-    iIntros "H". by iDestruct (HP with "H") as "$". }
+    iExists _. iIntros "H". by iDestruct (HP with "H") as "$". }
   rewrite -wp_bind. eapply bi.wand_apply;
     [by eapply bi.wand_entails, (recv_spec _ n (tele_app tv) (tele_app tP') (tele_app tp))|f_equiv; first done].
   rewrite -bi.later_intro; apply bi.forall_intro=> x.