diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 6ff8c238b7c0b962002cef90e48aaa8f70927b98..33ac6a46a968c70e639d060fd8516bab94ac10fe 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -28,10 +28,10 @@ variables:
 
 ## Build jobs
 
-build-coq.8.18.0:
+build-coq.8.20.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.18.0"
+    OPAM_PINS: "coq version 8.20.0"
     DENY_WARNINGS: "1"
     OPAM_PKG: "1"
   tags:
diff --git a/_CoqProject b/_CoqProject
index f25af835c52ada3a6b091f2d1fc14087b93513a0..77a40ad54ffbdfb45cac34eb2883775a341f0c4b 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -5,8 +5,6 @@
 # Cannot use non-canonical projections as it causes massive unification failures
 # (https://github.com/coq/coq/issues/6294).
 -arg -w -arg -redundant-canonical-projection
-# Fixing this one requires Coq 8.19
--arg -w -arg -argument-scope-delimiter
 
 theories/utils/llist.v
 theories/utils/compare.v
diff --git a/coq-actris.opam b/coq-actris.opam
index 08e7857a9583c960e63b6fccd5c0ee71275340ee..0f0153afb1d1c9ef7fc76cdd2870f19ced3da274 100644
--- a/coq-actris.opam
+++ b/coq-actris.opam
@@ -8,7 +8,7 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/actris/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/iris/actris.git"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2024-03-12.0.c1e15cdc") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2024-10-30.0.27f837c1") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 2c53a5efd81612ed04999d4c02582563080c988b..d6f23c512836246666e07610be06241b186e9fdf 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -68,46 +68,37 @@ Definition recv : val :=
 
 (** * Setup of Iris's cameras *)
 Class chanG Σ := {
-  chanG_lockG :: lockG Σ;
-  chanG_protoG :: protoG Σ val;
+  #[local] chanG_lockG :: lockG Σ;
+  #[local] chanG_protoG :: protoG Σ val;
 }.
 Definition chanΣ : gFunctors := #[ spin_lockΣ; protoΣ val ].
 Global Instance subG_chanΣ {Σ} : subG chanΣ Σ → chanG Σ.
 Proof. solve_inG. Qed.
 
-Record chan_name := ChanName {
-  chan_lock_name : gname;
-  chan_proto_name : proto_name;
-}.
-Global Instance chan_name_inhabited : Inhabited chan_name :=
-  populate (ChanName inhabitant inhabitant).
-Global Instance chan_name_eq_dec : EqDecision chan_name.
-Proof. solve_decision. Qed.
-Global Instance chan_name_countable : Countable chan_name.
-Proof.
- refine (inj_countable (λ '(ChanName γl γr), (γl,γr))
-   (λ '(γl, γr), Some (ChanName γl γr)) _); by intros [].
-Qed.
-
 (** * Definition of the pointsto connective *)
 Notation iProto Σ := (iProto Σ val).
 Notation iMsg Σ := (iMsg Σ val).
 
+Definition iProto_lock_inv `{!heapGS Σ, !chanG Σ}
+    (l r : loc) (γl γr : gname) : iProp Σ :=
+  ∃ vsl vsr,
+    llist internal_eq l vsl ∗
+    llist internal_eq r vsr ∗
+    steps_lb (length vsl) ∗ steps_lb (length vsr) ∗
+    iProto_ctx γl γr vsl vsr.
+
 Definition iProto_pointsto_def `{!heapGS Σ, !chanG Σ}
     (c : val) (p : iProto Σ) : iProp Σ :=
-  ∃ γ s (l r : loc) (lk : val),
-    ⌜ c = ((#(side_elim s l r), #(side_elim s r l)), lk)%V ⌝ ∗
-    is_lock (chan_lock_name γ) lk (∃ vsl vsr,
-      llist internal_eq l vsl ∗
-      llist internal_eq r vsr ∗
-      steps_lb (length vsl) ∗ steps_lb (length vsr) ∗
-      iProto_ctx (chan_proto_name γ) vsl vsr) ∗
-    iProto_own (chan_proto_name γ) s p.
+  ∃ γl γr γlk (l r : loc) (lk : val),
+    ⌜ c = ((#l, #r), lk)%V ⌝ ∗
+    is_lock γlk lk (iProto_lock_inv l r γl γr) ∗
+    iProto_own γl p.
+
 Definition iProto_pointsto_aux : seal (@iProto_pointsto_def). by eexists. Qed.
 Definition iProto_pointsto := iProto_pointsto_aux.(unseal).
 Definition iProto_pointsto_eq :
   @iProto_pointsto = @iProto_pointsto_def := iProto_pointsto_aux.(seal_eq).
-Arguments iProto_pointsto {_ _ _} _ _%proto.
+Arguments iProto_pointsto {_ _ _} _ _%_proto.
 Global Instance: Params (@iProto_pointsto) 4 := {}.
 Notation "c ↣ p" := (iProto_pointsto c p)
   (at level 20, format "c  ↣  p").
@@ -120,7 +111,7 @@ Definition iProto_choice {Σ} (a : action) (P1 P2 : iProp Σ)
     (p1 p2 : iProto Σ) : iProto Σ :=
   (<a @ (b : bool)> MSG #b {{ if b then P1 else P2 }}; if b then p1 else p2)%proto.
 Global Typeclasses Opaque iProto_choice.
-Arguments iProto_choice {_} _ _%I _%I _%proto _%proto.
+Arguments iProto_choice {_} _ _%_I _%_I _%_proto _%_proto.
 Global Instance: Params (@iProto_choice) 2 := {}.
 Infix "<{ P1 }+{ P2 }>" := (iProto_choice Send P1 P2) (at level 85) : proto_scope.
 Infix "<{ P1 }&{ P2 }>" := (iProto_choice Recv P1 P2) (at level 85) : proto_scope.
@@ -143,8 +134,8 @@ Section channel.
 
   Lemma iProto_pointsto_le c p1 p2 : c ↣ p1 ⊢ ▷ (p1 ⊑ p2) -∗ c ↣ p2.
   Proof.
-    rewrite iProto_pointsto_eq. iDestruct 1 as (γ s l r lk ->) "[Hlk H]".
-    iIntros "Hle'". iExists γ, s, l, r, lk. iSplit; [done|]. iFrame "Hlk".
+    rewrite iProto_pointsto_eq. iDestruct 1 as (γl γr γlk l r lk ->) "[Hlk H]".
+    iIntros "Hle'". iExists γl, γr, γlk, l, r, lk. iSplit; [done|]. iFrame "Hlk".
     by iApply (iProto_own_le with "H").
   Qed.
 
@@ -200,6 +191,13 @@ Section channel.
       iDestruct ("H" with "HP") as "[$ ?]"; by iModIntro.
   Qed.
 
+  Lemma iProto_lock_inv_sym l r γl γr :
+    iProto_lock_inv l r γl γr ⊢ iProto_lock_inv r l γr γl.
+  Proof.
+    iIntros "(%vsl & %vsr & Hlistl & Hlistr & Hstepsl & Hstepsr & Hctx)".
+    iExists vsr, vsl. iFrame. by iApply iProto_ctx_sym.
+  Qed.
+
   (** ** Specifications of [send] and [recv] *)
   Lemma new_chan_spec p :
     {{{ True }}}
@@ -209,16 +207,20 @@ Section channel.
     iIntros (Φ _) "HΦ". wp_lam. iMod (steps_lb_0) as "#Hlb".
     wp_smart_apply (lnil_spec internal_eq with "[//]"); iIntros (l) "Hl".
     wp_smart_apply (lnil_spec internal_eq with "[//]"); iIntros (r) "Hr".
-    iMod (iProto_init p) as (γp) "(Hctx & Hcl & Hcr)".
+    iMod (iProto_init p) as (γl γr) "(Hctx & Hcl & Hcr)".
     wp_smart_apply (newlock_spec (∃ vsl vsr,
       llist internal_eq l vsl ∗ llist internal_eq r vsr ∗
       steps_lb (length vsl) ∗ steps_lb (length vsr) ∗
-      iProto_ctx γp vsl vsr) with "[Hl Hr Hctx]").
+      iProto_ctx γl γr vsl vsr) with "[Hl Hr Hctx]").
     { iExists [], []. iFrame "#∗". }
     iIntros (lk γlk) "#Hlk". wp_pures. iApply "HΦ".
-    set (γ := ChanName γlk γp). iSplitL "Hcl".
-    - rewrite iProto_pointsto_eq. iExists γ, Left, l, r, lk. by iFrame "Hcl #".
-    - rewrite iProto_pointsto_eq. iExists γ, Right, l, r, lk. by iFrame "Hcr #".
+    iSplitL "Hcl".
+    - rewrite iProto_pointsto_eq.
+      iExists γl, γr, γlk, l, r, lk. by iFrame "Hcl #".
+    - rewrite iProto_pointsto_eq.
+      iExists γr, γl, γlk, r, l, lk. iFrame "Hcr #".
+      iModIntro. iSplit; first done. iApply (is_lock_iff with "Hlk").
+      iIntros "!> !>". iSplit; iIntros; by iApply iProto_lock_inv_sym.
   Qed.
 
   Lemma fork_chan_spec p Φ (f : val) :
@@ -239,50 +241,29 @@ Section channel.
     {{{ RET #(); c ↣ p }}}.
   Proof.
     rewrite iProto_pointsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
-    iDestruct "Hc" as (γ s l r lk ->) "[#Hlk H]"; wp_pures.
+    iDestruct "Hc" as (γl γr γlk l r lk ->) "[#Hlk H]"; wp_pures.
     wp_smart_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
     iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & #Hlbl & #Hlbr & Hctx)".
-    destruct s; simpl.
-    - wp_pures. wp_bind (lsnoc _ _).
-      iApply (wp_step_fupdN_lb with "Hlbr [Hctx H]"); [done| |].
-      { iApply fupd_mask_intro; [set_solver|]. simpl.
-        iIntros "Hclose !>!>".
-        iMod (iProto_send_l with "Hctx H []") as "[Hctx H]".
-        { rewrite iMsg_base_eq /=; auto. }
-        iModIntro.
-        iApply step_fupdN_intro; [done|].
-        iIntros "!>". iMod "Hclose".
-        iCombine ("Hctx H") as "H".
-        iExact "H". }
-      iApply (wp_lb_update with "Hlbl").
-      wp_smart_apply (lsnoc_spec with "[$Hl //]"); iIntros "Hl".
-      iIntros "#Hlbl' [Hctx H] !>".
-      wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]").
-      { iExists (vsl ++ [v]), vsr.
-        rewrite app_length /=.
-        replace (length vsl + 1) with (S (length vsl)) by lia.
-        iFrame "#∗". }
-      iIntros "_". iApply "HΦ". iExists γ, Left, l, r, lk. eauto 10 with iFrame.
-    - wp_pures. wp_bind (lsnoc _ _).
-      iApply (wp_step_fupdN_lb with "Hlbl [Hctx H]"); [done| |].
-      { iApply fupd_mask_intro; [set_solver|]. simpl.
-        iIntros "Hclose !>!>".
-        iMod (iProto_send_r with "Hctx H []") as "[Hctx H]".
-        { rewrite iMsg_base_eq /=; auto. }
-        iModIntro.
-        iApply step_fupdN_intro; [done|].
-        iIntros "!>". iMod "Hclose".
-        iCombine ("Hctx H") as "H".
-        iExact "H". }
-      iApply (wp_lb_update with "Hlbr").
-      wp_smart_apply (lsnoc_spec with "[$Hr //]"); iIntros "Hr".
-      iIntros "#Hlbr' [Hctx H] !>".
-      wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]").
-      { iExists vsl, (vsr ++ [v]).
-        rewrite app_length /=.
-        replace (length vsr + 1) with (S (length vsr)) by lia.
-        iFrame "#∗". }
-      iIntros "_". iApply "HΦ". iExists γ, Right, l, r, lk. eauto 10 with iFrame.
+    wp_pures. wp_bind (lsnoc _ _).
+    iApply (wp_step_fupdN_lb with "Hlbr [Hctx H]"); [done| |].
+    { iApply fupd_mask_intro; [set_solver|]. simpl.
+      iIntros "Hclose !>!>".
+      iMod (iProto_send with "Hctx H []") as "[Hctx H]".
+      { rewrite iMsg_base_eq /=; auto. }
+      iModIntro.
+      iApply step_fupdN_intro; [done|].
+      iIntros "!>". iMod "Hclose".
+      iCombine ("Hctx H") as "H".
+      iExact "H". }
+    iApply (wp_lb_update with "Hlbl").
+    wp_smart_apply (lsnoc_spec with "[$Hl //]"); iIntros "Hl".
+    iIntros "#Hlbl' [Hctx H] !>".
+    wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]").
+    { iExists (vsl ++ [v]), vsr.
+      rewrite length_app /=.
+      replace (length vsl + 1) with (S (length vsl)) by lia.
+      iFrame "#∗". }
+    iIntros "_". iApply "HΦ". iExists γl, γr, γlk. eauto 10 with iFrame.
   Qed.
 
   Lemma send_spec_tele {TT} c (tt : TT)
@@ -308,36 +289,25 @@ Section channel.
                   (∃.. x, ⌜w = SOMEV (v x)⌝ ∗ c ↣ p x ∗ P x) }}}.
   Proof.
     rewrite iProto_pointsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
-    iDestruct "Hc" as (γ s l r lk ->) "[#Hlk H]"; wp_pures.
+    iDestruct "Hc" as (γl γr γlk l r lk ->) "[#Hlk H]"; wp_pures.
     wp_smart_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
-    iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & #Hlbl & #Hlbr & Hctx)". destruct s; simpl.
-    - wp_smart_apply (lisnil_spec with "Hr"); iIntros "Hr".
-      destruct vsr as [|vr vsr]; wp_pures.
-      { wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
-        iIntros "_". wp_pures. iModIntro. iApply "HΦ". iLeft. iSplit; [done|].
-        iExists γ, Left, l, r, lk. eauto 10 with iFrame. }
-      wp_smart_apply (lpop_spec with "Hr"); iIntros (v') "[% Hr]"; simplify_eq/=.
-      iMod (iProto_recv_l with "Hctx H") as (q) "(Hctx & H & Hm)". wp_pures.
+    iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & #Hlbl & #Hlbr & Hctx)".
+    wp_smart_apply (lisnil_spec with "Hr"); iIntros "Hr".
+    destruct vsr as [|vr vsr]; wp_pures.
+    - wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]").
+      { unfold iProto_lock_inv; by eauto with iFrame. }
+      iIntros "_". wp_pures. iModIntro. iApply "HΦ". iLeft. iSplit; [done|].
+      iExists γl, γr, γlk. eauto 10 with iFrame.
+    - wp_smart_apply (lpop_spec with "Hr"); iIntros (v') "[% Hr]"; simplify_eq/=.
+      iMod (iProto_recv with "Hctx H") as (q) "(Hctx & H & Hm)". wp_pures.
       rewrite iMsg_base_eq.
       iDestruct (iMsg_texist_exist with "Hm") as (x <-) "[Hp HP]".
       iDestruct (steps_lb_le _ (length vsr) with "Hlbr") as "#Hlbr'"; [lia|].
-      wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
-      iIntros "_". wp_pures. iModIntro. iApply "HΦ". iRight. iExists x. iSplit; [done|].
-      iFrame "HP". iExists γ, Left, l, r, lk. iSplit; [done|]. iFrame "Hlk".
-      by iRewrite "Hp".
-    - wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl".
-      destruct vsl as [|vl vsl]; wp_pures.
-      { wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
-        iIntros "_". wp_pures. iModIntro. iApply "HΦ". iLeft. iSplit; [done|].
-        iExists γ, Right, l, r, lk. eauto 10 with iFrame. }
-      wp_smart_apply (lpop_spec with "Hl"); iIntros (v') "[% Hl]"; simplify_eq/=.
-      iMod (iProto_recv_r with "Hctx H") as (q) "(Hctx & H & Hm)". wp_pures.
-      rewrite iMsg_base_eq.
-      iDestruct (iMsg_texist_exist with "Hm") as (x <-) "[Hp HP]".
-      iDestruct (steps_lb_le _ (length vsl) with "Hlbl") as "#Hlbl'"; [lia|].
-      wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
-      iIntros "_". wp_pures. iModIntro. iApply "HΦ". iRight. iExists x. iSplit; [done|].
-      iFrame "HP". iExists γ, Right, l, r, lk. iSplit; [done|]. iFrame "Hlk".
+      wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]").
+      { unfold iProto_lock_inv; by eauto with iFrame. }
+      iIntros "_". wp_pures. iModIntro. iApply "HΦ".
+      iRight. iExists x. iSplit; [done|].
+      iFrame "HP". iExists γl, γr, γlk, l, r, lk. iSplit; [done|]. iFrame "Hlk".
       by iRewrite "Hp".
   Qed.
 
diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index 4fb801a61101c199ca72dcbe747add97094a838d..c8e5f414ec9fb28113e73bff947714d1c1362eff 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -36,7 +36,7 @@ Class ProtoNormalize {Σ} (d : bool) (p : iProto Σ)
     ⊢ iProto_dual_if d p <++>
         foldr (iProto_app ∘ uncurry iProto_dual_if) END%proto pas ⊑ q.
 Global Hint Mode ProtoNormalize ! ! ! ! - : typeclass_instances.
-Arguments ProtoNormalize {_} _ _%proto _%proto _%proto.
+Arguments ProtoNormalize {_} _ _%_proto _%_proto _%_proto.
 
 Notation ProtoUnfold p1 p2 := (∀ d pas q,
   ProtoNormalize d p2 pas q → ProtoNormalize d p1 pas q).
@@ -46,7 +46,7 @@ Class MsgNormalize {Σ} (d : bool) (m1 : iMsg Σ)
   msg_normalize a :
     ProtoNormalize d (<a> m1) pas (<(if d then action_dual a else a)> m2).
 Global Hint Mode MsgNormalize ! ! ! ! - : typeclass_instances.
-Arguments MsgNormalize {_} _ _%msg _%msg _%msg.
+Arguments MsgNormalize {_} _ _%_msg _%_msg _%_msg.
 
 Section classes.
   Context `{!chanG Σ, !heapGS Σ}.
@@ -241,37 +241,9 @@ Tactic Notation "wp_recv" "as" constr(pat) :=
 
 Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" constr(pat) :=
   wp_recv_core (intros xs) as (fun H => iDestructHyp H as pat).
-Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1) ")"
-    constr(pat) :=
-  wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 ) pat).
-Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
-    simple_intropattern(x2) ")" constr(pat) :=
-  wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 ) pat).
-Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
-    simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
-  wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 ) pat).
-Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
-    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
-    constr(pat) :=
-  wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 ) pat).
-Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
-    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
-    simple_intropattern(x5) ")" constr(pat) :=
-  wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
-Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
-    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
-    simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
-  wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
-Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
-    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
-    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
-    constr(pat) :=
-  wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
-Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
-    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
-    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
-    simple_intropattern(x8) ")" constr(pat) :=
-  wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
+Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as"
+    "(" ne_simple_intropattern_list(ys) ")" constr(pat) :=
+  wp_recv_core (intros xs) as (fun H => _iDestructHyp H ys pat).
 
 Lemma tac_wp_send `{!chanG Σ, !heapGS Σ} {TT : tele} Δ neg i js K c v p m tv tP tp Φ :
   envs_lookup i Δ = Some (false, c ↣ p)%I →
@@ -347,31 +319,8 @@ Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) :=
 
 Tactic Notation "wp_send" "with" constr(pat) :=
   wp_send_core (idtac) with pat.
-Tactic Notation "wp_send" "(" uconstr(x1) ")" "with" constr(pat) :=
-  wp_send_core (eexists x1) with pat.
-Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) ")" "with" constr(pat) :=
-  wp_send_core (eexists x1; eexists x2) with pat.
-Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) ")"
-    "with" constr(pat) :=
-  wp_send_core (eexists x1; eexists x2; eexists x3) with pat.
-Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")"
-    "with" constr(pat) :=
-  wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4) with pat.
-Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4)
-    uconstr(x5) ")" "with" constr(pat) :=
-  wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5) with pat.
-Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")"
-    uconstr(x5) uconstr(x6) ")" "with" constr(pat) :=
-  wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5;
-                eexists x6) with pat.
-Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")"
-    uconstr(x5) uconstr(x6) uconstr(x7) ")" "with" constr(pat) :=
-  wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5;
-                eexists x6; eexists x7) with pat.
-Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")"
-    uconstr(x5) uconstr(x6) uconstr(x7) uconstr(x8) ")" "with" constr(pat) :=
-  wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5;
-                eexists x6; eexists x7; eexists x8) with pat.
+Tactic Notation "wp_send" "(" ne_uconstr_list(xs) ")" "with" constr(pat) :=
+  wp_send_core (ltac1_list_iter ltac:(fun x => eexists x) xs) with pat.
 
 Lemma tac_wp_branch `{!chanG Σ, !heapGS Σ} Δ i j K
     c p P1 P2 (p1 p2 : iProto Σ) Φ :
@@ -501,5 +450,4 @@ Tactic Notation "wp_fork_chan" constr(prot) "as"
   wp_fork_chan prot as c pat and c pat.
 
 Tactic Notation "wp_fork_chan" constr(prot) :=
-  let iNew := iFresh in
-  wp_fork_chan prot as ? iNew.
+  wp_fork_chan prot as ? "?".
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index 9e9dfcfbfc71854310044ceafa0e101b9ac1849d..531c87151c572faeaa87200f05f0e159520f0ab3 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -108,7 +108,7 @@ Next Obligation. solve_proper. Qed.
 Definition iMsg_base_aux : seal (@iMsg_base_def). by eexists. Qed.
 Definition iMsg_base := iMsg_base_aux.(unseal).
 Definition iMsg_base_eq : @iMsg_base = @iMsg_base_def := iMsg_base_aux.(seal_eq).
-Arguments iMsg_base {_ _} _%V _%I _%proto.
+Arguments iMsg_base {_ _} _%_V _%_I _%_proto.
 Global Instance: Params (@iMsg_base) 3 := {}.
 
 Program Definition iMsg_exist_def {Σ V A} (m : A → iMsg Σ V) : iMsg Σ V :=
@@ -117,12 +117,12 @@ Next Obligation. solve_proper. Qed.
 Definition iMsg_exist_aux : seal (@iMsg_exist_def). by eexists. Qed.
 Definition iMsg_exist := iMsg_exist_aux.(unseal).
 Definition iMsg_exist_eq : @iMsg_exist = @iMsg_exist_def := iMsg_exist_aux.(seal_eq).
-Arguments iMsg_exist {_ _ _} _%msg.
+Arguments iMsg_exist {_ _ _} _%_msg.
 Global Instance: Params (@iMsg_exist) 3 := {}.
 
 Definition iMsg_texist {Σ V} {TT : tele} (m : TT → iMsg Σ V) : iMsg Σ V :=
   tele_fold (@iMsg_exist Σ V) (λ x, x) (tele_bind m).
-Arguments iMsg_texist {_ _ !_} _%msg /.
+Arguments iMsg_texist {_ _ !_} _%_msg /.
 
 Notation "'MSG' v {{ P } } ; p" := (iMsg_base v P p)
   (at level 200, v at level 20, right associativity,
@@ -157,7 +157,7 @@ Definition iProto_message_aux : seal (@iProto_message_def). by eexists. Qed.
 Definition iProto_message := iProto_message_aux.(unseal).
 Definition iProto_message_eq :
   @iProto_message = @iProto_message_def := iProto_message_aux.(seal_eq).
-Arguments iProto_message {_ _} _ _%msg.
+Arguments iProto_message {_ _} _ _%_msg.
 Global Instance: Params (@iProto_message) 3 := {}.
 
 Notation "'END'" := iProto_end : proto_scope.
@@ -225,7 +225,7 @@ Definition iProto_app_def {Σ V} (p1 p2 : iProto Σ V) : iProto Σ V :=
 Definition iProto_app_aux : seal (@iProto_app_def). Proof. by eexists. Qed.
 Definition iProto_app := iProto_app_aux.(unseal).
 Definition iProto_app_eq : @iProto_app = @iProto_app_def := iProto_app_aux.(seal_eq).
-Arguments iProto_app {_ _} _%proto _%proto.
+Arguments iProto_app {_ _} _%_proto _%_proto.
 Global Instance: Params (@iProto_app) 2 := {}.
 Infix "<++>" := iProto_app (at level 60) : proto_scope.
 Notation "m <++> p" := (iMsg_map (flip iProto_app p) m) : msg_scope.
@@ -236,13 +236,13 @@ Definition iProto_dual_aux : seal (@iProto_dual_def). Proof. by eexists. Qed.
 Definition iProto_dual := iProto_dual_aux.(unseal).
 Definition iProto_dual_eq :
   @iProto_dual = @iProto_dual_def := iProto_dual_aux.(seal_eq).
-Arguments iProto_dual {_ _} _%proto.
+Arguments iProto_dual {_ _} _%_proto.
 Global Instance: Params (@iProto_dual) 2 := {}.
 Notation iMsg_dual := (iMsg_map iProto_dual).
 
 Definition iProto_dual_if {Σ V} (d : bool) (p : iProto Σ V) : iProto Σ V :=
   if d then iProto_dual p else p.
-Arguments iProto_dual_if {_ _} _ _%proto.
+Arguments iProto_dual_if {_ _} _ _%_proto.
 Global Instance: Params (@iProto_dual_if) 3 := {}.
 
 (** * Protocol entailment *)
@@ -277,7 +277,7 @@ Proof.
 Qed.
 Definition iProto_le {Σ V} (p1 p2 : iProto Σ V) : iProp Σ :=
   fixpoint iProto_le_pre' p1 p2.
-Arguments iProto_le {_ _} _%proto _%proto.
+Arguments iProto_le {_ _} _%_proto _%_proto.
 Global Instance: Params (@iProto_le) 2 := {}.
 Notation "p ⊑ q" := (iProto_le p q) : bi_scope.
 
@@ -294,52 +294,33 @@ Fixpoint iProto_app_recvs {Σ V} (vs : list V) (p : iProto Σ V) : iProto Σ V :
 Definition iProto_interp {Σ V} (vsl vsr : list V) (pl pr : iProto Σ V) : iProp Σ :=
   ∃ p, iProto_app_recvs vsr p ⊑ pl ∗ iProto_app_recvs vsl (iProto_dual p) ⊑ pr.
 
-Record proto_name := ProtName { proto_l_name : gname; proto_r_name : gname }.
-Global Instance proto_name_inhabited : Inhabited proto_name :=
-  populate (ProtName inhabitant inhabitant).
-Global Instance proto_name_eq_dec : EqDecision proto_name.
-Proof. solve_decision. Qed.
-Global Instance proto_name_countable : Countable proto_name.
-Proof.
- refine (inj_countable (λ '(ProtName γl γr), (γl,γr))
-   (λ '(γl, γr), Some (ProtName γl γr)) _); by intros [].
-Qed.
-
-Inductive side := Left | Right.
-Global Instance side_inhabited : Inhabited side := populate Left.
-Global Instance side_eq_dec : EqDecision side.
-Proof. solve_decision. Qed.
-Global Instance side_countable : Countable side.
-Proof.
- refine (inj_countable (λ s, if s is Left then true else false)
-   (λ b, Some (if b then Left else Right)) _); by intros [].
-Qed.
-Definition side_elim {A} (s : side) (l r : A) : A :=
-  match s with Left => l | Right => r end.
-
-Definition iProto_own_frag `{!protoG Σ V} (γ : proto_name) (s : side)
+Definition iProto_own_frag `{!protoG Σ V} (γ : gname)
     (p : iProto Σ V) : iProp Σ :=
-  own (side_elim s proto_l_name proto_r_name γ) (◯E (Next p)).
-Definition iProto_own_auth `{!protoG Σ V} (γ : proto_name) (s : side)
+  own γ (◯E (Next p)).
+Definition iProto_own_auth `{!protoG Σ V} (γ : gname)
     (p : iProto Σ V) : iProp Σ :=
-  own (side_elim s proto_l_name proto_r_name γ) (●E (Next p)).
+  own γ (●E (Next p)).
 
+(** In the original Actris papers we a single ghost name for [iProto_ctx] and
+[iProto_own]. To distinguish the two [iProto_own]s for both sides, we used
+an enum [Left]/[Right]. This turned out to be cumbersome because at various
+places we need to case at this enum. The current version of [iProto_ctx] has two
+ghost names, one for each [iProto_own], enabling more uniform definitions. *)
 Definition iProto_ctx `{protoG Σ V}
-    (γ : proto_name) (vsl vsr : list V) : iProp Σ :=
+    (γl γr : gname) (vsl vsr : list V) : iProp Σ :=
   ∃ pl pr,
-    iProto_own_auth γ Left pl ∗
-    iProto_own_auth γ Right pr ∗
+    iProto_own_auth γl pl ∗
+    iProto_own_auth γr pr ∗
     â–· iProto_interp vsl vsr pl pr.
 
 (** * The connective for ownership of channel ends *)
-Definition iProto_own `{!protoG Σ V}
-    (γ : proto_name) (s : side) (p : iProto Σ V) : iProp Σ :=
-  ∃ p', ▷ (p' ⊑ p) ∗ iProto_own_frag γ s p'.
-Arguments iProto_own {_ _ _} _ _%proto.
-Global Instance: Params (@iProto_own) 3 := {}.
-
-Global Instance iProto_own_contractive `{protoG Σ V} γ s :
-  Contractive (iProto_own γ s).
+Definition iProto_own `{!protoG Σ V} (γ : gname) (p : iProto Σ V) : iProp Σ :=
+  ∃ p', ▷ (p' ⊑ p) ∗ iProto_own_frag γ p'.
+Arguments iProto_own {_ _ _} _ _%_proto.
+Global Instance: Params (@iProto_own) 4 := {}.
+
+Global Instance iProto_own_contractive `{protoG Σ V} γ :
+  Contractive (iProto_own γ).
 Proof. solve_contractive. Qed.
 
 (** * Proofs *)
@@ -1026,20 +1007,20 @@ Section proto.
     Proper ((≡) ==> (≡) ==> (≡)) (iProto_interp (Σ:=Σ) (V:=V) vsl vsr).
   Proof. apply (ne_proper_2 _). Qed.
 
-  Global Instance iProto_own_frag_ne γ s : NonExpansive (iProto_own_frag γ s).
+  Global Instance iProto_own_frag_ne γ : NonExpansive (iProto_own_frag γ).
   Proof. solve_proper. Qed.
 
-  Lemma iProto_own_auth_agree γ s p p' :
-    iProto_own_auth γ s p -∗ iProto_own_frag γ s p' -∗ ▷ (p ≡ p').
+  Lemma iProto_own_auth_agree γ p p' :
+    iProto_own_auth γ p -∗ iProto_own_frag γ p' -∗ ▷ (p ≡ p').
   Proof.
     iIntros "H● H◯". iCombine "H● H◯" gives "H✓".
     iDestruct (excl_auth_agreeI with "H✓") as "{H✓} H✓".
     iApply (later_equivI_1 with "H✓").
   Qed.
 
-  Lemma iProto_own_auth_update γ s p p' p'' :
-    iProto_own_auth γ s p -∗ iProto_own_frag γ s p' ==∗
-    iProto_own_auth γ s p'' ∗ iProto_own_frag γ s p''.
+  Lemma iProto_own_auth_update γ p p' p'' :
+    iProto_own_auth γ p -∗ iProto_own_frag γ p' ==∗
+    iProto_own_auth γ p'' ∗ iProto_own_frag γ p''.
   Proof.
     iIntros "H● H◯". iDestruct (own_update_2 with "H● H◯") as "H".
     { eapply (excl_auth_update _ _ (Next p'')). }
@@ -1049,8 +1030,8 @@ Section proto.
   Lemma iProto_interp_nil p : ⊢ iProto_interp [] [] p (iProto_dual p).
   Proof. iExists p; simpl. iSplitL; iApply iProto_le_refl. Qed.
 
-  Lemma iProto_interp_flip vsl vsr pl pr :
-    iProto_interp vsl vsr pl pr -∗ iProto_interp vsr vsl pr pl.
+  Lemma iProto_interp_sym vsl vsr pl pr :
+    iProto_interp vsl vsr pl pr ⊢ iProto_interp vsr vsl pr pl.
   Proof.
     iDestruct 1 as (p) "[Hp Hdp]". iExists (iProto_dual p).
     rewrite (involutive iProto_dual). iFrame.
@@ -1065,8 +1046,8 @@ Section proto.
   Lemma iProto_interp_le_r vsl vsr pl pr pr' :
     iProto_interp vsl vsr pl pr -∗ pr ⊑ pr' -∗ iProto_interp vsl vsr pl pr'.
   Proof.
-    iIntros "H Hle". iApply iProto_interp_flip.
-    iApply (iProto_interp_le_l with "[H] Hle"). by iApply iProto_interp_flip.
+    iIntros "H Hle". iApply iProto_interp_sym.
+    iApply (iProto_interp_le_l with "[H] Hle"). by iApply iProto_interp_sym.
   Qed.
 
   Lemma iProto_interp_send vl ml vsl vsr pr pl' :
@@ -1107,39 +1088,47 @@ Section proto.
     iExists pr''. iIntros "{$Hpr} !>". iExists p. iFrame.
   Qed.
 
-  Global Instance iProto_own_ne γ s : NonExpansive (iProto_own γ s).
+  Lemma iProto_ctx_sym γl γr vsl vsr :
+    iProto_ctx γl γr vsl vsr ⊢ iProto_ctx γr γl vsr vsl.
+  Proof.
+    iIntros "(%pl & %pr & Hauthl & Hauthr & Hinterp)".
+    iDestruct (iProto_interp_sym with "Hinterp") as "Hinterp".
+    iExists pr, pl; iFrame.
+  Qed.
+
+  Global Instance iProto_own_ne γ : NonExpansive (iProto_own γ).
   Proof. solve_proper. Qed.
-  Global Instance iProto_own_proper γ s : Proper ((≡) ==> (≡)) (iProto_own γ s).
+  Global Instance iProto_own_proper γ : Proper ((≡) ==> (≡)) (iProto_own γ).
   Proof. apply (ne_proper _). Qed.
 
-  Lemma iProto_own_le γ s p1 p2 :
-    iProto_own γ s p1 -∗ ▷ (p1 ⊑ p2) -∗ iProto_own γ s p2.
+  Lemma iProto_own_le γ p1 p2 :
+    iProto_own γ p1 -∗ ▷ (p1 ⊑ p2) -∗ iProto_own γ p2.
   Proof.
     iDestruct 1 as (p1') "[Hle H]". iIntros "Hle'".
     iExists p1'. iFrame "H". by iApply (iProto_le_trans with "Hle").
   Qed.
 
   Lemma iProto_init p :
-    ⊢ |==> ∃ γ,
-      iProto_ctx γ [] [] ∗
-      iProto_own γ Left p ∗ iProto_own γ Right (iProto_dual p).
+    ⊢ |==> ∃ γl γr,
+      iProto_ctx γl γr [] [] ∗
+      iProto_own γl p ∗ iProto_own γr (iProto_dual p).
   Proof.
-    iMod (own_alloc (●E (Next p) ⋅ ◯E (Next p))) as (lγ) "[H●l H◯l]".
+    iMod (own_alloc (●E (Next p) ⋅ ◯E (Next p))) as (γl) "[H●l H◯l]".
     { by apply excl_auth_valid. }
     iMod (own_alloc (●E (Next (iProto_dual p)) ⋅
-      ◯E (Next (iProto_dual p)))) as (rγ) "[H●r H◯r]".
+      ◯E (Next (iProto_dual p)))) as (γr) "[H●r H◯r]".
     { by apply excl_auth_valid. }
-    pose (ProtName lγ rγ) as γ. iModIntro. iExists γ. iSplitL "H●l H●r".
+    iModIntro. iExists γl, γr. iSplitL "H●l H●r".
     { iExists p, (iProto_dual p). iFrame. iApply iProto_interp_nil. }
     iSplitL "Hâ—¯l"; iExists _; iFrame; iApply iProto_le_refl.
   Qed.
 
-  Lemma iProto_send_l γ m vsr vsl vl p :
-    iProto_ctx γ vsl vsr -∗
-    iProto_own γ Left (<!> m) -∗
+  Lemma iProto_send γl γr m vsr vsl vl p :
+    iProto_ctx γl γr vsl vsr -∗
+    iProto_own γl (<!> m) -∗
     iMsg_car m vl (Next p) ==∗
-      ▷^(length vsr) iProto_ctx γ (vsl ++ [vl]) vsr ∗
-      iProto_own γ Left p.
+      ▷^(length vsr) iProto_ctx γl γr (vsl ++ [vl]) vsr ∗
+      iProto_own γl p.
   Proof.
     iDestruct 1 as (pl pr) "(H●l & H●r & Hinterp)".
     iDestruct 1 as (pl') "[Hle Hâ—¯]". iIntros "Hm".
@@ -1148,39 +1137,18 @@ Section proto.
       with "[Hle]" as "{Hp} Hle"; first (iNext; by iRewrite "Hp").
     iDestruct (iProto_interp_le_l with "Hinterp Hle") as "Hinterp".
     iDestruct (iProto_interp_send with "Hinterp [Hm //]") as "Hinterp".
-    iMod (iProto_own_auth_update _ _ _ _ p with "H●l H◯") as "[H●l H◯]".
+    iMod (iProto_own_auth_update _ _ _ p with "H●l H◯") as "[H●l H◯]".
     iIntros "!>". iSplitR "Hâ—¯".
     - iIntros "!>". iExists p, pr. iFrame.
     - iExists p. iFrame. iApply iProto_le_refl.
   Qed.
 
-  Lemma iProto_send_r γ m vsr vsl vr p :
-    iProto_ctx γ vsl vsr -∗
-    iProto_own γ Right (<!> m) -∗
-    iMsg_car m vr (Next p) ==∗
-      ▷^(length vsl) iProto_ctx γ vsl (vsr ++ [vr]) ∗
-      iProto_own γ Right p.
-  Proof.
-    iDestruct 1 as (pl pr) "(H●l & H●r & Hinterp)".
-    iDestruct 1 as (pr') "[Hle Hâ—¯]". iIntros "Hm".
-    iDestruct (iProto_own_auth_agree with "H●r H◯") as "#Hp".
-    iAssert (▷ (pr ⊑ <!> m))%I
-      with "[Hle]" as "{Hp} Hle"; first (iNext; by iRewrite "Hp").
-    iDestruct (iProto_interp_flip with "Hinterp") as "Hinterp".
-    iDestruct (iProto_interp_le_l with "Hinterp Hle") as "Hinterp".
-    iDestruct (iProto_interp_send with "Hinterp [Hm //]") as "Hinterp".
-    iMod (iProto_own_auth_update _ _ _ _ p with "H●r H◯") as "[H●r H◯]".
-    iIntros "!>". iSplitR "Hâ—¯".
-    - iIntros "!>". iExists pl, p. iFrame. by iApply iProto_interp_flip.
-    - iExists p. iFrame. iApply iProto_le_refl.
-  Qed.
-
-  Lemma iProto_recv_l γ m vr vsr vsl :
-    iProto_ctx γ vsl (vr :: vsr) -∗
-    iProto_own γ Left (<?> m) ==∗
+  Lemma iProto_recv γl γr m vr vsr vsl :
+    iProto_ctx γl γr vsl (vr :: vsr) -∗
+    iProto_own γl (<?> m) ==∗
     ▷ ∃ p,
-      iProto_ctx γ vsl vsr ∗
-      iProto_own γ Left p ∗
+      iProto_ctx γl γr vsl vsr ∗
+      iProto_own γl p ∗
       iMsg_car m vr (Next p).
   Proof.
     iDestruct 1 as (pl pr) "(H●l & H●r & Hinterp)".
@@ -1188,31 +1156,11 @@ Section proto.
     iDestruct (iProto_own_auth_agree with "H●l H◯") as "#Hp".
     iDestruct (iProto_interp_le_l with "Hinterp [Hle]") as "Hinterp".
     { iIntros "!>". by iRewrite "Hp". }
-    iDestruct (iProto_interp_flip with "Hinterp") as "Hinterp".
-    iDestruct (iProto_interp_recv with "Hinterp") as (q) "[Hm Hinterp]".
-    iMod (iProto_own_auth_update _ _ _ _ q with "H●l H◯") as "[H●l H◯]".
-    iIntros "!> !> /=". iExists q. iFrame "Hm". iSplitR "Hâ—¯".
-    - iExists q, pr. iFrame. by iApply iProto_interp_flip.
-    - iExists q. iIntros "{$Hâ—¯} !>". iApply iProto_le_refl.
-  Qed.
-
-  Lemma iProto_recv_r γ m vl vsr vsl :
-    iProto_ctx γ (vl :: vsl) vsr -∗
-    iProto_own γ Right (<?> m) ==∗
-    ▷ ∃ p,
-      iProto_ctx γ vsl vsr ∗
-      iProto_own γ Right p ∗
-      iMsg_car m vl (Next p).
-  Proof.
-    iDestruct 1 as (pl pr) "(H●l & H●r & Hinterp)".
-    iDestruct 1 as (p) "[Hle Hâ—¯]".
-    iDestruct (iProto_own_auth_agree with "H●r H◯") as "#Hp".
-    iDestruct (iProto_interp_le_r with "Hinterp [Hle]") as "Hinterp".
-    { iIntros "!>". by iRewrite "Hp". }
+    iDestruct (iProto_interp_sym with "Hinterp") as "Hinterp".
     iDestruct (iProto_interp_recv with "Hinterp") as (q) "[Hm Hinterp]".
-    iMod (iProto_own_auth_update _ _ _ _ q with "H●r H◯") as "[H●r H◯]".
+    iMod (iProto_own_auth_update _ _ _ q with "H●l H◯") as "[H●l H◯]".
     iIntros "!> !> /=". iExists q. iFrame "Hm". iSplitR "Hâ—¯".
-    - iExists pl, q. iFrame.
+    - iExists q, pr. iFrame. by iApply iProto_interp_sym.
     - iExists q. iIntros "{$Hâ—¯} !>". iApply iProto_le_refl.
   Qed.
 
diff --git a/theories/examples/pizza.v b/theories/examples/pizza.v
index b5674883171d4e9738fa22a3f5fedc976e1fe6ac..c0d9a33e63b7977a788b56e7d47d10de7a2626c2 100644
--- a/theories/examples/pizza.v
+++ b/theories/examples/pizza.v
@@ -129,7 +129,7 @@ Section example.
        "v2")
     ).
 
-  Lemma lock_example_spec jcc rcc c (x1 y1 : Z) :
+  Lemma lock_example_spec `{!lockG Σ} jcc rcc c (x1 y1 : Z) :
     {{{ c ↣ pizza_prot ∗ jcc ↦ #x1 ∗ rcc ↦ #y1 }}}
       lock_example #jcc #rcc c
     {{{ (x2 y2 : Z), RET ((#x2, #(x1 - x2)), (#y2, #(y1 - y2)))%V;
diff --git a/theories/logrel/examples/par_recv.v b/theories/logrel/examples/par_recv.v
index fb9a56d4dcc89f8a098a20347f3c0dea718416de..b512bc099a5743ada8f94abb1ad7ac3c467a1907 100755
--- a/theories/logrel/examples/par_recv.v
+++ b/theories/logrel/examples/par_recv.v
@@ -35,7 +35,7 @@ Definition prog : val := λ: "c",
   ).
 
 Section double.
-  Context `{heapGS Σ, chanG Σ, spawnG Σ}.
+  Context `{!heapGS Σ, !chanG Σ, !spawnG Σ, !lockG Σ}.
   Context `{!inG Σ fracR}.
 
   Definition prog_prot : iProto Σ :=
@@ -119,7 +119,7 @@ Section double.
 End double.
 
 Section double_fc.
-  Context `{heapGS Σ, chanG Σ, spawnG Σ}.
+  Context `{!heapGS Σ, !chanG Σ, !spawnG Σ, !lockG Σ}.
   Context `{!inG Σ (exclR unitO), inG Σ (prodR fracR (agreeR (optionO valO)))}.
 
   Definition prog_prot_fc (P : val → val → iProp Σ) : iProto Σ :=
diff --git a/theories/logrel/model.v b/theories/logrel/model.v
index dad84550896cff0816aace2029cb9062585273ea..10a435909fe17d3b857d67ca0d7b75db686b2bf2 100644
--- a/theories/logrel/model.v
+++ b/theories/logrel/model.v
@@ -24,8 +24,8 @@ Global Instance kind_inhabited : Inhabited kind := populate tty_kind.
 Variant lty Σ : kind → Type :=
   | Ltty : (val → iProp Σ) → lty Σ tty_kind
   | Lsty : iProto Σ → lty Σ sty_kind.
-Arguments Ltty {_} _%I.
-Arguments Lsty {_} _%proto.
+Arguments Ltty {_} _%_I.
+Arguments Lsty {_} _%_proto.
 
 Declare Scope lty_scope.
 Bind Scope lty_scope with lty.
diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index 95af463ed698183989145ece118c3fa1ca11c0fc..d1a27efcccb4998a7f20049eaab0cbf1f219dae6 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -19,7 +19,7 @@ Definition lty_msg_exist {Σ} {k} (M : lty Σ k → lmsg Σ) : lmsg Σ :=
 
 Definition lty_msg_texist {Σ} {kt : ktele Σ} (M : ltys Σ kt → lmsg Σ) : lmsg Σ :=
   ktele_fold (@lty_msg_exist Σ) (λ x, x) (ktele_bind M).
-Arguments lty_msg_texist {_ !_} _%lmsg /.
+Arguments lty_msg_texist {_ !_} _%_lmsg /.
 
 Definition lty_end {Σ} : lsty Σ := Lsty END.
 
@@ -108,7 +108,7 @@ Section session_types.
   Global Instance lty_choice_proper a : Proper ((≡) ==> (≡)) (@lty_choice Σ a).
   Proof. apply ne_proper, _. Qed.
   Global Instance lty_choice_contractive a n :
-    Proper (map_relation (dist_later n) (λ _, False) (λ _, False) ==> dist n)
+    Proper (map_relation (λ _, dist_later n) (λ _ _, False) (λ _ _, False) ==> dist n)
            (@lty_choice Σ a).
   Proof.
     intros Ss Ts Heq. rewrite /lty_choice.
diff --git a/theories/logrel/session_typing_rules.v b/theories/logrel/session_typing_rules.v
index 5cac0e12a7b5810ddbb42c933cd9bbed5631731f..5dfafee1f3d22af759defdff5d2bc19523cf59e5 100644
--- a/theories/logrel/session_typing_rules.v
+++ b/theories/logrel/session_typing_rules.v
@@ -181,7 +181,7 @@ Section session_typing_rules.
     iIntros (Hdom) "!>". iIntros (vs) "$". iApply wp_value.
     iIntros (c) "Hc". wp_lam.
     rewrite -subst_map_singleton.
-    iApply lty_arr_list_spec; [by rewrite fmap_length|].
+    iApply lty_arr_list_spec; [by rewrite length_fmap|].
     iIntros (ws) "H".
     rewrite big_sepL2_fmap_l.
     iDestruct (big_sepL2_length with "H") as %Heq.