diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 2c53a5efd81612ed04999d4c02582563080c988b..52e10620358daa91fa14b5b64f42110d90f56414 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -75,34 +75,25 @@ 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 :
@@ -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 app_length /=.
+      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/proto.v b/theories/channel/proto.v
index 9e9dfcfbfc71854310044ceafa0e101b9ac1849d..e91572234343b4de84df7964e4da76bb562fb5a0 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -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'.
+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) 3 := {}.
+Global Instance: Params (@iProto_own) 4 := {}.
 
-Global Instance iProto_own_contractive `{protoG Σ V} γ s :
-  Contractive (iProto_own γ s).
+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.