diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index 460f565be97081045503274bfa66a49028b198ff..ea2a2e8af662bd0ee7b527c6e8a37df41b2236ae 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -48,7 +48,7 @@ Notation ProtoUnfold p1 p2 := (∀ d pas q,
   ProtoNormalize d p2 pas q → ProtoNormalize d p1 pas q).
 
 Section classes.
-  Context `{!proto_chanG Σ, !heapG Σ} (N : namespace).
+  Context `{!proto_chanG Σ, !heapG Σ}.
   Implicit Types p : iProto Σ.
   Implicit Types TT : tele.
 
@@ -139,14 +139,14 @@ Section classes.
   (** Automatically perform normalization of protocols in the proof mode *)
   Global Instance mapsto_proto_from_assumption q c p1 p2 :
     ProtoNormalize false p1 [] p2 →
-    FromAssumption q (c ↣ p1 @ N) (c ↣ p2 @ N).
+    FromAssumption q (c ↣ p1) (c ↣ p2).
   Proof.
     rewrite /FromAssumption /ProtoNormalize=> ->.
     by rewrite /= right_id bi.intuitionistically_if_elim.
   Qed.
   Global Instance mapsto_proto_from_frame q c p1 p2 :
     ProtoNormalize false p1 [] p2 →
-    Frame q (c ↣ p1 @ N) (c ↣ p2 @ N) True.
+    Frame q (c ↣ p1) (c ↣ p2) True.
   Proof.
     rewrite /Frame /ProtoNormalize=> ->.
     by rewrite /= !right_id bi.intuitionistically_if_elim.
@@ -155,14 +155,14 @@ End classes.
 
 (** Symbolic execution tactics *)
 (* TODO: strip laters *)
-Lemma tac_wp_recv `{!proto_chanG Σ, !heapG Σ} {TT : tele} Δ i j K N
+Lemma tac_wp_recv `{!proto_chanG Σ, !heapG Σ} {TT : tele} Δ i j K
     c p (pc : TT → val * iProp Σ * iProto Σ) Φ :
-  envs_lookup i Δ = Some (false, c ↣ p @ N)%I →
+  envs_lookup i Δ = Some (false, c ↣ p)%I →
   ProtoNormalize false p [] (iProto_message Receive pc) →
   let Δ' := envs_delete false i false Δ in
   (∀.. x : TT,
     match envs_app false
-        (Esnoc (Esnoc Enil j ((pc x).1.2)) i (c ↣ (pc x).2 @ N)) Δ' with
+        (Esnoc (Esnoc Enil j ((pc x).1.2)) i (c ↣ (pc x).2)) Δ' with
     | Some Δ'' => envs_entails Δ'' (WP fill K (of_val (pc x).1.1) {{ Φ }})
     | None => False
     end) →
@@ -179,7 +179,7 @@ Qed.
 
 Tactic Notation "wp_recv_core" tactic3(tac_intros) "as" tactic3(tac) :=
   let solve_mapsto _ :=
-    let c := match goal with |- _ = Some (_, (?c ↣ _ @ _)%I) => c end in
+    let c := match goal with |- _ = Some (_, (?c ↣ _)%I) => c end in
     iAssumptionCore || fail "wp_recv: cannot find" c "↣ ? @ ?" in
   wp_pures;
   let Hnew := iFresh in
@@ -233,15 +233,15 @@ Tactic Notation "wp_recv" "(" intropattern_list(xs) ")" "as" "(" simple_intropat
     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).
 
-Lemma tac_wp_send `{!proto_chanG Σ, !heapG Σ} {TT : tele} Δ neg i js K N
+Lemma tac_wp_send `{!proto_chanG Σ, !heapG Σ} {TT : tele} Δ neg i js K
     c v p (pc : TT → val * iProp Σ * iProto Σ) Φ :
-  envs_lookup i Δ = Some (false, c ↣ p @ N)%I →
+  envs_lookup i Δ = Some (false, c ↣ p)%I →
   ProtoNormalize false p [] (iProto_message Send pc) →
   let Δ' := envs_delete false i false Δ in
   (∃.. x : TT,
     match envs_split (if neg is true then Right else Left) js Δ' with
     | Some (Δ1,Δ2) =>
-       match envs_app false (Esnoc Enil i (c ↣ (pc x).2 @ N)) Δ2 with
+       match envs_app false (Esnoc Enil i (c ↣ (pc x).2)) Δ2 with
        | Some Δ2' =>
           v = (pc x).1.1 ∧
           envs_entails Δ1 (pc x).1.2 ∧
@@ -265,7 +265,7 @@ Qed.
 
 Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) :=
   let solve_mapsto _ :=
-    let c := match goal with |- _ = Some (_, (?c ↣ _ @ _)%I) => c end in
+    let c := match goal with |- _ = Some (_, (?c ↣ _)%I) => c end in
     iAssumptionCore || fail "wp_send: cannot find" c "↣ ? @ ?" in
   let solve_done d :=
     lazymatch d with
@@ -327,14 +327,14 @@ Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")
   wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5;
                 eexists x6; eexists x7; eexists x8) with pat.
 
-Lemma tac_wp_branch `{!proto_chanG Σ, !heapG Σ} Δ i j K N
+Lemma tac_wp_branch `{!proto_chanG Σ, !heapG Σ} Δ i j K
     c p P1 P2 (p1 p2 : iProto Σ) Φ :
-  envs_lookup i Δ = Some (false, c ↣ p @ N)%I →
+  envs_lookup i Δ = Some (false, c ↣ p)%I →
   ProtoNormalize false p [] (p1 <{P1}&{P2}> p2) →
   let Δ' := envs_delete false i false Δ in
   (∀ b : bool,
     match envs_app false
-        (Esnoc (Esnoc Enil j (if b then P1 else P2)) i (c ↣ (if b then p1 else p2) @ N)) Δ' with
+        (Esnoc (Esnoc Enil j (if b then P1 else P2)) i (c ↣ (if b then p1 else p2))) Δ' with
     | Some Δ'' => envs_entails Δ'' (WP fill K (of_val #b) {{ Φ }})
     | None => False
     end) →
@@ -350,7 +350,7 @@ Qed.
 
 Tactic Notation "wp_branch_core" "as" tactic3(tac1) tactic3(tac2) :=
   let solve_mapsto _ :=
-    let c := match goal with |- _ = Some (_, (?c ↣ _ @ _)%I) => c end in
+    let c := match goal with |- _ = Some (_, (?c ↣ _)%I) => c end in
     iAssumptionCore || fail "wp_branch: cannot find" c "↣ ? @ ?" in
   wp_pures;
   let Hnew := iFresh in
@@ -375,14 +375,14 @@ Tactic Notation "wp_branch" "as" "%" intropattern(pat1) "|" "%" intropattern(pat
   wp_branch_core as (fun H => iPure H as pat1) (fun H => iPure H as pat2).
 Tactic Notation "wp_branch" := wp_branch as %_ | %_.
 
-Lemma tac_wp_select `{!proto_chanG Σ, !heapG Σ} Δ neg i js K N
+Lemma tac_wp_select `{!proto_chanG Σ, !heapG Σ} Δ neg i js K
     c (b : bool) p P1 P2 (p1 p2 : iProto Σ) Φ :
-  envs_lookup i Δ = Some (false, c ↣ p @ N)%I →
+  envs_lookup i Δ = Some (false, c ↣ p)%I →
   ProtoNormalize false p [] (p1 <{P1}+{P2}> p2) →
   let Δ' := envs_delete false i false Δ in
   match envs_split (if neg is true then Right else Left) js Δ' with
   | Some (Δ1,Δ2) =>
-     match envs_app false (Esnoc Enil i (c ↣ if b then p1 else p2 @ N)) Δ2 with
+     match envs_app false (Esnoc Enil i (c ↣ if b then p1 else p2)) Δ2 with
      | Some Δ2' =>
         envs_entails Δ1 (if b then P1 else P2) ∧
         envs_entails Δ2' (WP fill K (of_val #()) {{ Φ }})
@@ -404,7 +404,7 @@ Qed.
 
 Tactic Notation "wp_select" "with" constr(pat) :=
   let solve_mapsto _ :=
-    let c := match goal with |- _ = Some (_, (?c ↣ _ @ _)%I) => c end in
+    let c := match goal with |- _ = Some (_, (?c ↣ _)%I) => c end in
     iAssumptionCore || fail "wp_select: cannot find" c "↣ ? @ ?" in
   let solve_done d :=
     lazymatch d with
diff --git a/theories/channel/proto_channel.v b/theories/channel/proto_channel.v
index ff3ab045313a82452f20861e098243cfc5ccdcc0..0e3995cc96b92f1f6da491a5e3d199b0e56a23fb 100644
--- a/theories/channel/proto_channel.v
+++ b/theories/channel/proto_channel.v
@@ -191,22 +191,24 @@ Definition proto_inv `{!proto_chanG Σ} (γ : proto_name) : iProp Σ :=
     ▷ ((⌜r = []⌝ ∗ proto_eval l pl pr) ∨
        (⌜l = []⌝ ∗ proto_eval r pr pl)))%I.
 
-Definition mapsto_proto_def `{!proto_chanG Σ, !heapG Σ} (N : namespace)
+Definition protoN := nroot .@ "proto".
+
+Definition mapsto_proto_def `{!proto_chanG Σ, !heapG Σ}
     (c : val) (p : iProto Σ) : iProp Σ :=
   (∃ s (c1 c2 : val) γ,
     ⌜ c = side_elim s c1 c2 ⌝ ∗
-    proto_own_frag γ s p ∗ is_chan N (proto_c_name γ) c1 c2 ∗ inv N (proto_inv γ))%I.
+    proto_own_frag γ s p ∗ is_chan protoN (proto_c_name γ) c1 c2 ∗ inv protoN (proto_inv γ))%I.
 Definition mapsto_proto_aux : seal (@mapsto_proto_def). by eexists. Qed.
 Definition mapsto_proto {Σ pΣ hΣ} := mapsto_proto_aux.(unseal) Σ pΣ hΣ.
 Definition mapsto_proto_eq : @mapsto_proto = @mapsto_proto_def := mapsto_proto_aux.(seal_eq).
-Arguments mapsto_proto {_ _ _} _ _ _%proto.
-Instance: Params (@mapsto_proto) 5 := {}.
+Arguments mapsto_proto {_ _ _} _ _%proto.
+Instance: Params (@mapsto_proto) 4 := {}.
 
-Notation "c ↣ p @ N" := (mapsto_proto N c p)
-  (at level 20, N at level 50, format "c  ↣  p  @  N").
+Notation "c ↣ p" := (mapsto_proto c p)
+  (at level 20, format "c  ↣  p").
 
 Section proto.
-  Context `{!proto_chanG Σ, !heapG Σ} (N : namespace).
+  Context `{!proto_chanG Σ, !heapG Σ}.
   Implicit Types p : iProto Σ.
   Implicit Types TT : tele.
 
@@ -344,9 +346,9 @@ Section proto.
   Proof. solve_proper. Qed.
   Global Instance proto_own_ne γ s : NonExpansive (proto_own_frag γ s).
   Proof. solve_proper. Qed.
-  Global Instance mapsto_proto_ne c : NonExpansive (mapsto_proto N c).
+  Global Instance mapsto_proto_ne c : NonExpansive (mapsto_proto c).
   Proof. rewrite mapsto_proto_eq. solve_proper. Qed.
-  Global Instance mapsto_proto_proper c : Proper ((≡) ==> (≡)) (mapsto_proto N c).
+  Global Instance mapsto_proto_proper c : Proper ((≡) ==> (≡)) (mapsto_proto c).
   Proof. apply (ne_proper _). Qed.
 
   Lemma proto_own_auth_agree γ s p p' :
@@ -416,9 +418,9 @@ Section proto.
 
   (** The actual specs *)
   Lemma proto_init E cγ c1 c2 p :
-    is_chan N cγ c1 c2 -∗
+    is_chan protoN cγ c1 c2 -∗
     chan_own cγ Left [] -∗ chan_own cγ Right [] ={E}=∗
-    c1 ↣ p @ N ∗ c2 ↣ iProto_dual p @ N.
+    c1 ↣ p ∗ c2 ↣ iProto_dual p.
   Proof.
     iIntros "#Hcctx Hcol Hcor".
     iMod (own_alloc (● (to_proto_auth_excl p) ⋅
@@ -428,7 +430,7 @@ Section proto.
                      ◯ (to_proto_auth_excl (iProto_dual p)))) as (rγ) "[Hrsta Hrstf]".
     { by apply auth_both_valid_2. }
     pose (ProtName cγ lγ rγ) as pγ.
-    iMod (inv_alloc N _ (proto_inv pγ) with "[-Hlstf Hrstf Hcctx]") as "#Hinv".
+    iMod (inv_alloc protoN _ (proto_inv pγ) with "[-Hlstf Hrstf Hcctx]") as "#Hinv".
     { iNext. rewrite /proto_inv. eauto 10 with iFrame. }
     iModIntro. rewrite mapsto_proto_eq. iSplitL "Hlstf".
     - iExists Left, c1, c2, pγ; iFrame; auto.
@@ -437,20 +439,20 @@ Section proto.
 
   (** Accessor style lemmas *)
   Lemma proto_send_acc {TT} E c (pc : TT → val * iProp Σ * iProto Σ) :
-    ↑N ⊆ E →
-    c ↣ iProto_message Send pc @ N -∗ ∃ s c1 c2 γ,
+    ↑protoN ⊆ E →
+    c ↣ iProto_message Send pc -∗ ∃ s c1 c2 γ,
       ⌜ c = side_elim s c1 c2 ⌝ ∗
-      is_chan N (proto_c_name γ) c1 c2 ∗ |={E,E∖↑N}=> ∃ vs,
+      is_chan protoN (proto_c_name γ) c1 c2 ∗ |={E,E∖↑protoN}=> ∃ vs,
         chan_own (proto_c_name γ) s vs ∗
         ▷ ∀ (x : TT),
            (pc x).1.2 -∗
-           chan_own (proto_c_name γ) s (vs ++ [(pc x).1.1]) ={E∖↑N,E}=∗
-           c ↣ (pc x).2 @ N.
+           chan_own (proto_c_name γ) s (vs ++ [(pc x).1.1]) ={E∖↑protoN,E}=∗
+           c ↣ (pc x).2.
   Proof.
     iIntros (?). rewrite {1}mapsto_proto_eq iProto_message_eq.
     iDestruct 1 as (s c1 c2 γ ->) "[Hstf #[Hcctx Hinv]]".
     iExists s, c1, c2, γ. iSplit; first done. iFrame "Hcctx".
-    iInv N as (l r pl pr) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose".
+    iInv protoN as (l r pl pr) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose".
     (* TODO: refactor to avoid twice nearly the same proof *)
     iModIntro. destruct s.
     - iExists _.
@@ -494,23 +496,23 @@ Section proto.
   Qed.
 
   Lemma proto_recv_acc {TT} E c (pc : TT → val * iProp Σ * iProto Σ) :
-    ↑N ⊆ E →
-    c ↣ iProto_message Receive pc @ N -∗ ∃ s c1 c2 γ,
+    ↑protoN ⊆ E →
+    c ↣ iProto_message Receive pc -∗ ∃ s c1 c2 γ,
       ⌜ c = side_elim s c2 c1 ⌝ ∗
-      is_chan N (proto_c_name γ) c1 c2 ∗ |={E,E∖↑N}=> ∃ vs,
+      is_chan protoN (proto_c_name γ) c1 c2 ∗ |={E,E∖↑protoN}=> ∃ vs,
         chan_own (proto_c_name γ) s vs ∗
-        ▷ ((chan_own (proto_c_name γ) s vs ={E∖↑N,E}=∗
-             c ↣ iProto_message Receive pc @ N) ∧
+        ▷ ((chan_own (proto_c_name γ) s vs ={E∖↑protoN,E}=∗
+             c ↣ iProto_message Receive pc) ∧
            (∀ v vs',
              ⌜ vs = v :: vs' ⌝ -∗
-             chan_own (proto_c_name γ) s vs' ={E∖↑N,E}=∗ ▷ ▷ ∃ x : TT,
-             ⌜ v = (pc x).1.1 ⌝ ∗ c ↣ (pc x).2 @ N ∗ (pc x).1.2)).
+             chan_own (proto_c_name γ) s vs' ={E∖↑protoN,E}=∗ ▷ ▷ ∃ x : TT,
+             ⌜ v = (pc x).1.1 ⌝ ∗ c ↣ (pc x).2 ∗ (pc x).1.2)).
   Proof.
     iIntros (?). rewrite {1}mapsto_proto_eq iProto_message_eq.
     iDestruct 1 as (s c1 c2 γ ->) "[Hstf #[Hcctx Hinv]]".
     iExists (side_elim s Right Left), c1, c2, γ. iSplit; first by destruct s.
     iFrame "Hcctx".
-    iInv N as (l r pl pr) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose".
+    iInv protoN as (l r pl pr) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose".
     iExists (side_elim s r l). iModIntro.
     (* TODO: refactor to avoid twice nearly the same proof *)
     destruct s; simpl.
@@ -533,7 +535,7 @@ Section proto.
         iMod ("Hclose" with "[-Hstlf Hf]") as %_.
         { iExists _, _,_ ,_. eauto 10 with iFrame. }
         iIntros "!> !>".
-        set (f lp := (∃ q, lp ≡ Next q ∧ c1 ↣ q @ N)%I).
+        set (f lp := (∃ q, lp ≡ Next q ∧ c1 ↣ q)%I).
         assert (NonExpansive f) by solve_proper.
         iDestruct ("Hf" $! (OfeMor f) with "[Hstlf]") as (x) "(Hv & HP & Hf) /=".
         { iExists q. iSplit; first done. rewrite mapsto_proto_eq.
@@ -559,7 +561,7 @@ Section proto.
         iMod ("Hclose" with "[-Hstrf Hf]") as %_.
         { iExists _, _, _, _. eauto 10 with iFrame. }
         iIntros "!> !>".
-        set (f lp := (∃ q, lp ≡ Next q ∧ c2 ↣ q @ N)%I).
+        set (f lp := (∃ q, lp ≡ Next q ∧ c2 ↣ q)%I).
         assert (NonExpansive f) by solve_proper.
         iDestruct ("Hf" $! (OfeMor f) with "[Hstrf]") as (x) "(Hv & HP & Hf) /=".
         { iExists q. iSplit; first done. rewrite mapsto_proto_eq.
@@ -572,7 +574,7 @@ Section proto.
   Lemma new_chan_proto_spec :
     {{{ True }}}
       new_chan #()
-    {{{ c1 c2, RET (c1,c2); (∀ p, |={⊤}=> c1 ↣ p @ N ∗ c2 ↣ iProto_dual p @ N) }}}.
+    {{{ c1 c2, RET (c1,c2); (∀ p, |={⊤}=> c1 ↣ p ∗ c2 ↣ iProto_dual p) }}}.
   Proof.
     iIntros (Ψ _) "HΨ". iApply wp_fupd. wp_apply new_chan_spec=> //.
     iIntros (c1 c2 γ) "(Hc & Hl & Hr)". iApply "HΨ"; iIntros "!>" (p).
@@ -580,8 +582,8 @@ Section proto.
   Qed.
 
   Lemma start_chan_proto_spec p Ψ (f : val) :
-    ▷ (∀ c, c ↣ iProto_dual p @ N -∗ WP f c {{ _, True }}) -∗
-    ▷ (∀ c, c ↣ p @ N -∗ Ψ c) -∗
+    ▷ (∀ c, c ↣ iProto_dual p -∗ WP f c {{ _, True }}) -∗
+    ▷ (∀ c, c ↣ p -∗ Ψ c) -∗
     WP start_chan f {{ Ψ }}.
   Proof.
     iIntros "Hfork HΨ". wp_lam.
@@ -593,9 +595,9 @@ Section proto.
   Qed.
 
   Lemma send_proto_spec_packed {TT} c (pc : TT → val * iProp Σ * iProto Σ) (x : TT) :
-    {{{ c ↣ iProto_message Send pc @ N ∗ (pc x).1.2 }}}
+    {{{ c ↣ iProto_message Send pc ∗ (pc x).1.2 }}}
       send c (pc x).1.1
-    {{{ RET #(); c ↣ (pc x).2 @ N }}}.
+    {{{ RET #(); c ↣ (pc x).2 }}}.
   Proof.
     iIntros (Ψ) "[Hp Hf] HΨ".
     iDestruct (proto_send_acc ⊤ with "Hp") as (γ s c1 c2 ->) "[#Hc Hvs]"; first done.
@@ -606,9 +608,9 @@ Section proto.
   Qed.
 
   Lemma send_proto_spec {TT} Ψ c v (pc : TT → val * iProp Σ * iProto Σ) :
-    c ↣ iProto_message Send pc @ N -∗
+    c ↣ iProto_message Send pc -∗
     (∃.. x : TT,
-      ⌜ v = (pc x).1.1 ⌝ ∗ (pc x).1.2 ∗ ▷ (c ↣ (pc x).2 @ N -∗ Ψ #())) -∗
+      ⌜ v = (pc x).1.1 ⌝ ∗ (pc x).1.2 ∗ ▷ (c ↣ (pc x).2 -∗ Ψ #())) -∗
     WP send c v {{ Ψ }}.
   Proof.
     iIntros "Hc H". iDestruct (bi_texist_exist with "H") as (x ->) "[HP HΨ]".
@@ -616,10 +618,10 @@ Section proto.
   Qed.
 
   Lemma try_recv_proto_spec_packed {TT} c (pc : TT → val * iProp Σ * iProto Σ) :
-    {{{ c ↣ iProto_message Receive pc @ N }}}
+    {{{ c ↣ iProto_message Receive pc }}}
       try_recv c
-    {{{ v, RET v; (⌜v = NONEV⌝ ∧ c ↣ iProto_message Receive pc @ N) ∨
-                  (∃ x : TT, ⌜v = SOMEV ((pc x).1.1)⌝ ∗ c ↣ (pc x).2 @ N ∗ (pc x).1.2) }}}.
+    {{{ v, RET v; (⌜v = NONEV⌝ ∧ c ↣ iProto_message Receive pc) ∨
+                  (∃ x : TT, ⌜v = SOMEV ((pc x).1.1)⌝ ∗ c ↣ (pc x).2 ∗ (pc x).1.2) }}}.
   Proof.
     iIntros (Ψ) "Hp HΨ".
     iDestruct (proto_recv_acc ⊤ with "Hp") as (γ s c1 c2 ->) "[#Hc Hvs]"; first done.
@@ -633,9 +635,9 @@ Section proto.
   Qed.
 
   Lemma recv_proto_spec_packed {TT} c (pc : TT → val * iProp Σ * iProto Σ) :
-    {{{ c ↣ iProto_message Receive pc @ N }}}
+    {{{ c ↣ iProto_message Receive pc }}}
       recv c
-    {{{ x, RET (pc x).1.1; c ↣ (pc x).2 @ N ∗ (pc x).1.2 }}}.
+    {{{ x, RET (pc x).1.1; c ↣ (pc x).2 ∗ (pc x).1.2 }}}.
   Proof.
     iIntros (Ψ) "Hp HΨ".
     iDestruct (proto_recv_acc ⊤ with "Hp") as (γ s c1 c2 ->) "[#Hc Hvs]"; first done.
@@ -646,8 +648,8 @@ Section proto.
   Qed.
 
   Lemma recv_proto_spec {TT} Ψ c (pc : TT → val * iProp Σ * iProto Σ) :
-    c ↣ iProto_message Receive pc @ N -∗
-    ▷ (∀.. x : TT, c ↣ (pc x).2 @ N -∗ (pc x).1.2 -∗ Ψ (pc x).1.1) -∗
+    c ↣ iProto_message Receive pc -∗
+    ▷ (∀.. x : TT, c ↣ (pc x).2 -∗ (pc x).1.2 -∗ Ψ (pc x).1.1) -∗
     WP recv c {{ Ψ }}.
   Proof.
     iIntros "Hc H". iApply (recv_proto_spec_packed with "[$]").
@@ -657,18 +659,18 @@ Section proto.
 
   (** Branching *)
   Lemma select_spec c (b : bool) P1 P2 p1 p2 :
-    {{{ c ↣ p1 <{P1}+{P2}> p2 @ N ∗ if b then P1 else P2 }}}
+    {{{ c ↣ (p1 <{P1}+{P2}> p2) ∗ if b then P1 else P2 }}}
       send c #b
-    {{{ RET #(); c ↣ (if b then p1 else p2) @ N }}}.
+    {{{ RET #(); c ↣ (if b then p1 else p2) }}}.
   Proof.
     rewrite /iProto_branch. iIntros (Ψ) "[Hc HP] HΨ".
     iApply (send_proto_spec with "Hc"); simpl; eauto with iFrame.
   Qed.
 
   Lemma branch_spec c P1 P2 p1 p2 :
-    {{{ c ↣ p1 <{P1}&{P2}> p2 @ N }}}
+    {{{ c ↣ (p1 <{P1}&{P2}> p2) }}}
       recv c
-    {{{ b, RET #b; c ↣ if b : bool then p1 else p2 @ N ∗ if b then P1 else P2 }}}.
+    {{{ b, RET #b; c ↣ (if b : bool then p1 else p2) ∗ if b then P1 else P2 }}}.
   Proof.
     rewrite /iProto_branch. iIntros (Ψ) "Hc HΨ".
     iApply (recv_proto_spec with "Hc"); simpl.
diff --git a/theories/examples/basics.v b/theories/examples/basics.v
index 7f0daef3190f6d82c9a06bd4e3f1672d08c2a730..b1f8784a676a95119f5ff7999ff847f07f3f1802 100644
--- a/theories/examples/basics.v
+++ b/theories/examples/basics.v
@@ -47,7 +47,7 @@ Definition prot2 : iProto Σ :=
   (<?> l : loc, MSG #l {{ l ↦ #42 }}; END)%proto.
 
 Definition prot3 : iProto Σ :=
-  (<?> c : val, MSG c {{ c ↣ prot1 @ nroot }}; END)%proto.
+  (<?> c : val, MSG c {{ c ↣ prot1 }}; END)%proto.
 
 Definition prot4 : iProto Σ :=
   (<!> x : Z, MSG #x; <?> MSG #(x + 2); END)%proto.
@@ -68,7 +68,7 @@ Fixpoint prot_lock (n : nat) : iProto Σ :=
 Lemma prog1_spec : {{{ True }}} prog1 #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_proto_spec nroot prot1); iIntros (c) "Hc".
+  wp_apply (start_chan_proto_spec prot1); iIntros (c) "Hc".
   - by wp_send with "[]".
   - wp_recv as "_". by iApply "HΦ".
 Qed.
@@ -76,7 +76,7 @@ Qed.
 Lemma prog2_spec : {{{ True }}} prog2 #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_proto_spec nroot prot2); iIntros (c) "Hc".
+  wp_apply (start_chan_proto_spec prot2); iIntros (c) "Hc".
   - wp_alloc l as "Hl". by wp_send with "[$Hl]".
   - wp_recv (l) as "Hl". wp_load. by iApply "HΦ".
 Qed.
@@ -84,8 +84,8 @@ Qed.
 Lemma prog3_spec : {{{ True }}} prog3 #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_proto_spec nroot prot3); iIntros (c) "Hc".
-  - wp_apply (new_chan_proto_spec nroot with "[//]").
+  wp_apply (start_chan_proto_spec prot3); iIntros (c) "Hc".
+  - wp_apply (new_chan_proto_spec with "[//]").
     iIntros (c2 c2') "Hcc2". iMod ("Hcc2" $! prot1) as "[Hc2 Hc2']".
     wp_send with "[$Hc2]". by wp_send with "[]".
   - wp_recv (c2) as "Hc2". wp_recv as "_". by iApply "HΦ".
@@ -94,7 +94,7 @@ Qed.
 Lemma prog4_spec : {{{ True }}} prog4 #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_proto_spec nroot prot4); iIntros (c) "Hc".
+  wp_apply (start_chan_proto_spec prot4); iIntros (c) "Hc".
   - wp_recv (x) as "_". by wp_send with "[]".
   - wp_send with "[//]". wp_recv as "_". by iApply "HΦ".
 Qed.
@@ -102,7 +102,7 @@ Qed.
 Lemma prog5_spec : {{{ True }}} prog5 #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_proto_spec nroot prot5); iIntros (c) "Hc".
+  wp_apply (start_chan_proto_spec prot5); iIntros (c) "Hc".
   - wp_recv (P Ψ vf) as "#Hf". wp_send with "[]"; last done.
     iIntros "!>" (Ψ') "HP HΨ'". wp_apply ("Hf" with "HP"); iIntros (x) "HΨ".
     wp_pures. by iApply "HΨ'".
@@ -117,12 +117,12 @@ Lemma prog_lock_spec `{!lockG Σ, contributionG Σ unitUR} :
   {{{ True }}} prog_lock #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_proto_spec nroot (prot_lock 2)); iIntros (c) "Hc".
+  wp_apply (start_chan_proto_spec (prot_lock 2)); iIntros (c) "Hc".
   - iMod (contribution_init) as (γ) "Hs".
     iMod (alloc_client with "Hs") as "[Hs Hcl1]".
     iMod (alloc_client with "Hs") as "[Hs Hcl2]".
     wp_apply (newlock_spec nroot (∃ n, server γ n ε ∗
-      c ↣ iProto_dual (prot_lock n) @ nroot)%I
+      c ↣ iProto_dual (prot_lock n))%I
       with "[Hc Hs]"); first by eauto with iFrame.
     iIntros (lk γlk) "#Hlk".
     iAssert (□ (client γ ε -∗
diff --git a/theories/examples/loop_sort.v b/theories/examples/loop_sort.v
index 0ec452dfc43d55a3f24f7bb5f39c4e6f60ea5af2..296e1b42ae2d5b009333026a51aca17786944ae7 100644
--- a/theories/examples/loop_sort.v
+++ b/theories/examples/loop_sort.v
@@ -26,7 +26,7 @@ Definition sort_service_br_del : val :=
     else #().
 
 Section sort_service_br_del.
-  Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
+  Context `{!heapG Σ, !proto_chanG Σ}.
   Context {A} (I : A → val → iProp Σ) (R : A → A → Prop) `{!RelDecision R, !Total R}.
 
   Definition sort_protocol_br_aux (rec : iProto Σ) : iProto Σ :=
@@ -40,9 +40,9 @@ Section sort_service_br_del.
 
   Lemma sort_service_br_spec cmp c :
     cmp_spec I R cmp -∗
-    {{{ c ↣ iProto_dual sort_protocol_br @ N }}}
+    {{{ c ↣ iProto_dual sort_protocol_br }}}
       sort_service_br cmp c
-    {{{ RET #(); c ↣ END @ N }}}.
+    {{{ RET #(); c ↣ END }}}.
   Proof.
     iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (c Ψ).
     wp_rec. wp_branch; wp_pures.
@@ -52,7 +52,7 @@ Section sort_service_br_del.
   Qed.
 
   Definition sort_protocol_del_aux (rec : iProto Σ) : iProto Σ :=
-    ((<?> c, MSG c {{ c ↣ sort_protocol I R @ N }}; rec) <+> END)%proto.
+    ((<?> c, MSG c {{ c ↣ sort_protocol I R }}; rec) <+> END)%proto.
   Instance sort_protocol_del_aux_contractive : Contractive sort_protocol_del_aux.
   Proof. solve_proto_contractive. Qed.
   Definition sort_protocol_del : iProto Σ := fixpoint sort_protocol_del_aux.
@@ -62,13 +62,13 @@ Section sort_service_br_del.
 
   Lemma sort_protocol_del_spec cmp c :
     cmp_spec I R cmp -∗
-    {{{ c ↣ iProto_dual sort_protocol_del @ N }}}
+    {{{ c ↣ iProto_dual sort_protocol_del }}}
       sort_service_del cmp c
-    {{{ RET #(); c ↣ END @ N }}}.
+    {{{ RET #(); c ↣ END }}}.
   Proof.
     iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (Ψ).
     wp_rec. wp_branch; wp_pures.
-    { wp_apply (start_chan_proto_spec _ (sort_protocol I R <++> END)%proto);
+    { wp_apply (start_chan_proto_spec (sort_protocol I R <++> END)%proto);
         iIntros (c') "Hc'".
       { wp_pures. wp_apply (sort_service_spec with "Hcmp Hc'"); auto. }
       wp_send with "[$Hc']". by wp_apply ("IH" with "Hc"). }
@@ -76,7 +76,7 @@ Section sort_service_br_del.
   Qed.
 
   Definition sort_protocol_br_del_aux (rec : iProto Σ) : iProto Σ :=
-    ((sort_protocol I R <++> rec) <+> ((<?> c, MSG c {{ c ↣ rec @ N }}; rec) <+> END))%proto.
+    ((sort_protocol I R <++> rec) <+> ((<?> c, MSG c {{ c ↣ rec }}; rec) <+> END))%proto.
   Instance sort_protocol_br_del_aux_contractive : Contractive sort_protocol_br_del_aux.
   Proof. solve_proto_contractive. Qed.
   Definition sort_protocol_br_del : iProto Σ := fixpoint sort_protocol_br_del_aux.
@@ -86,16 +86,16 @@ Section sort_service_br_del.
 
   Lemma sort_service_br_del_spec cmp c :
     cmp_spec I R cmp -∗
-    {{{ c ↣ iProto_dual sort_protocol_br_del @ N }}}
+    {{{ c ↣ iProto_dual sort_protocol_br_del }}}
       sort_service_br_del cmp c
-    {{{ RET #(); c ↣ END @ N }}}.
+    {{{ RET #(); c ↣ END }}}.
   Proof.
     iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (c Ψ).
     wp_rec. wp_branch; wp_pures.
     { wp_apply (sort_service_spec with "Hcmp Hc"); iIntros "Hc".
       by wp_apply ("IH" with "Hc"). }
     wp_branch; wp_pures.
-    { wp_apply (start_chan_proto_spec N sort_protocol_br_del); iIntros (c') "Hc'".
+    { wp_apply (start_chan_proto_spec sort_protocol_br_del); iIntros (c') "Hc'".
       { wp_apply ("IH" with "Hc'"); auto. }
       wp_send with "[$Hc']".
       by wp_apply ("IH" with "Hc"). }
diff --git a/theories/examples/map.v b/theories/examples/map.v
index e3362d5d4793a58bce72c59f037e0f3d7697a235..76b65892ca34191801d0ca214acf9dbbd7c6bbdb 100644
--- a/theories/examples/map.v
+++ b/theories/examples/map.v
@@ -56,7 +56,7 @@ Class mapG Σ A `{Countable A} := {
 
 Section map.
   Context `{Countable A} {B : Type}.
-  Context `{!heapG Σ, !proto_chanG Σ, !mapG Σ A} (N : namespace).
+  Context `{!heapG Σ, !proto_chanG Σ, !mapG Σ A}.
   Context (IA : A → val → iProp Σ) (IB : B → val → iProp Σ) (map : A → list B).
   Local Open Scope nat_scope.
   Implicit Types n : nat.
@@ -82,11 +82,11 @@ Section map.
   Proof. apply proto_unfold_eq, (fixpoint_unfold par_map_protocol_aux). Qed.
 
   Definition map_worker_lock_inv (γ : gname) (c : val) : iProp Σ :=
-    (∃ i X, server γ i X ∗ c ↣ iProto_dual (par_map_protocol i X) @ N)%I.
+    (∃ i X, server γ i X ∗ c ↣ iProto_dual (par_map_protocol i X))%I.
 
   Lemma par_map_worker_spec γl γ vmap lk c :
     map_spec vmap -∗
-    {{{ is_lock N γl lk (map_worker_lock_inv γ c) ∗ client γ (∅ : gmultiset A) }}}
+    {{{ is_lock nroot γl lk (map_worker_lock_inv γ c) ∗ client γ (∅ : gmultiset A) }}}
       par_map_worker vmap lk c
     {{{ RET #(); True }}}.
   Proof.
@@ -126,7 +126,7 @@ Section map.
 
   Lemma par_map_workers_spec γl γ n vmap lk c :
     map_spec vmap -∗
-    {{{ is_lock N γl lk (map_worker_lock_inv γ c) ∗
+    {{{ is_lock nroot γl lk (map_worker_lock_inv γ c) ∗
         [∗] replicate n (client γ (∅:gmultiset A)) }}}
       par_map_workers #n vmap lk c
     {{{ RET #(); True }}}.
@@ -143,13 +143,13 @@ Section map.
 
   Lemma par_map_service_spec n vmap c :
     map_spec vmap -∗
-    {{{ c ↣ iProto_dual (par_map_protocol n ∅) @ N }}}
+    {{{ c ↣ iProto_dual (par_map_protocol n ∅) }}}
       par_map_service #n vmap c
     {{{ RET #(); True }}}.
   Proof.
     iIntros "#Hf !>"; iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
     iMod (contribution_init_pow (A:=gmultisetUR A) n) as (γ) "[Hs Hγs]".
-    wp_apply (newlock_spec N (map_worker_lock_inv γ c) with "[Hc Hs]").
+    wp_apply (newlock_spec nroot (map_worker_lock_inv γ c) with "[Hc Hs]").
     { iExists n, ∅. iFrame. }
     iIntros (lk γl) "#Hlk".
     wp_apply (par_map_workers_spec with "Hf [$Hlk $Hγs]"); auto.
@@ -157,7 +157,7 @@ Section map.
 
   Lemma par_map_client_loop_spec n c l k xs X ys :
     (n = 0 → X = ∅ ∧ xs = []) →
-    {{{ llist IA l xs ∗ llist IB k ys ∗ c ↣ par_map_protocol n X @ N }}}
+    {{{ llist IA l xs ∗ llist IB k ys ∗ c ↣ par_map_protocol n X }}}
       par_map_client_loop #n c #l #k
     {{{ ys', RET #();
       ⌜ys' ≡ₚ (xs ++ elements X) ≫= map⌝ ∗ llist IA l [] ∗ llist IB k (ys' ++ ys)
@@ -198,7 +198,7 @@ Section map.
     {{{ ys, RET #(); ⌜ys ≡ₚ xs ≫= map⌝ ∗ llist IB l ys }}}.
   Proof.
     iIntros (?) "#Hmap !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures.
-    wp_apply (start_chan_proto_spec N (par_map_protocol n ∅)); iIntros (c) "// Hc".
+    wp_apply (start_chan_proto_spec (par_map_protocol n ∅)); iIntros (c) "// Hc".
     { wp_apply (par_map_service_spec with "Hmap Hc"); auto. }
     wp_pures. wp_apply (lnil_spec with "[//]"); iIntros (k) "Hk".
     wp_apply (par_map_client_loop_spec with "[$Hl $Hk $Hc //]"); first lia.
diff --git a/theories/examples/map_reduce.v b/theories/examples/map_reduce.v
index 160824e14710290b070bcdf0406dc73c58b0eb0b..8a6fce25cc54e58077734c580e9a5c3326541493 100644
--- a/theories/examples/map_reduce.v
+++ b/theories/examples/map_reduce.v
@@ -95,7 +95,7 @@ Class map_reduceG Σ A B `{Countable A, Countable B} := {
 
 Section mapper.
   Context `{Countable A, Countable B} {C : Type}.
-  Context `{!heapG Σ, !proto_chanG Σ, !map_reduceG Σ A B} (N : namespace).
+  Context `{!heapG Σ, !proto_chanG Σ, !map_reduceG Σ A B}.
   Context (IA : A → val → iProp Σ) (IB : Z → B → val → iProp Σ) (IC : C → val → iProp Σ).
   Context (map : A → list (Z * B)) (red : Z → list B → list C).
   Context `{!∀ j, Proper ((≡ₚ) ==> (≡ₚ)) (red j)}.
@@ -127,13 +127,13 @@ Section mapper.
     (n = 0 → X = ∅ ∧ xs = []) →
     {{{
       llist IA l xs ∗
-      cmap ↣ par_map_protocol IA IZB map n (X : gmultiset A) @ N ∗
-      csort ↣ sort_fg_head_protocol IZB RZB ys @ N
+      cmap ↣ par_map_protocol IA IZB map n (X : gmultiset A) ∗
+      csort ↣ sort_fg_head_protocol IZB RZB ys
     }}}
       par_map_reduce_map #n cmap csort #l
     {{{ ys', RET #();
       ⌜ys' ≡ₚ (xs ++ elements X) ≫= map⌝ ∗
-      llist IA l [] ∗ csort ↣ sort_fg_head_protocol IZB RZB (ys ++ ys') @ N
+      llist IA l [] ∗ csort ↣ sort_fg_head_protocol IZB RZB (ys ++ ys')
     }}}.
   Proof.
     iIntros (Hn Φ) "(Hl & Hcmap & Hcsort) HΦ".
@@ -172,7 +172,7 @@ Section mapper.
     i ∉ iys_sorted.*1 →
     {{{
       llist (IB i) l (reverse ys) ∗
-      csort ↣ sort_fg_tail_protocol IZB RZB iys (iys_sorted ++ ((i,) <$> ys)) @ N
+      csort ↣ sort_fg_tail_protocol IZB RZB iys (iys_sorted ++ ((i,) <$> ys))
     }}}
       par_map_reduce_collect csort #i #l
     {{{ ys' miy, RET accv miy;
@@ -181,7 +181,7 @@ Section mapper.
                     (iys_sorted ++ ((i,) <$> ys ++ ys') ≡ₚ iys) miy ⌝ ∗
       llist (IB i) l (reverse (ys ++ ys')) ∗
       csort ↣ from_option (λ _, sort_fg_tail_protocol IZB RZB iys
-        ((iys_sorted ++ ((i,) <$> ys ++ ys')) ++ acc miy)) END%proto miy @ N ∗
+        ((iys_sorted ++ ((i,) <$> ys ++ ys')) ++ acc miy)) END%proto miy ∗
       from_option (λ '(i,y,w), IB i y w) True miy
     }}}.
   Proof.
@@ -222,8 +222,8 @@ Section mapper.
     {{{
       llist IC l zs ∗
       csort ↣ from_option (λ _, sort_fg_tail_protocol IZB RZB iys
-        (iys_sorted ++ acc miy)) END%proto miy @ N ∗
-      cred ↣ par_map_protocol IZBs IC (curry red) n (Y : gmultiset (Z * list B)) @ N ∗
+        (iys_sorted ++ acc miy)) END%proto miy ∗
+      cred ↣ par_map_protocol IZBs IC (curry red) n (Y : gmultiset (Z * list B)) ∗
       from_option (λ '(i,y,w), IB i y w) True miy
     }}}
       par_map_reduce_reduce #n csort cred (accv miy) #l
@@ -280,18 +280,18 @@ Section mapper.
     {{{ zs, RET #(); ⌜zs ≡ₚ map_reduce map red xs⌝ ∗ llist IC l zs }}}.
   Proof.
     iIntros (?) "#Hmap #Hred !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures.
-    wp_apply (start_chan_proto_spec N (par_map_protocol IA IZB map n ∅));
+    wp_apply (start_chan_proto_spec (par_map_protocol IA IZB map n ∅));
       iIntros (cmap) "// Hcmap".
     { wp_pures. wp_apply (par_map_service_spec with "Hmap Hcmap"); auto. }
-    wp_apply (start_chan_proto_spec N (sort_fg_protocol IZB RZB <++> END)%proto);
+    wp_apply (start_chan_proto_spec (sort_fg_protocol IZB RZB <++> END)%proto);
       iIntros (csort) "Hcsort".
-    { wp_apply (sort_service_fg_spec N with "[] Hcsort"); last by auto.
+    { wp_apply (sort_service_fg_spec with "[] Hcsort"); last by auto.
       iApply RZB_cmp_spec. }
     rewrite right_id.
     wp_apply (par_map_reduce_map_spec with "[$Hl $Hcmap $Hcsort]"); first lia.
     iIntros (iys). rewrite gmultiset_elements_empty right_id_L.
     iDestruct 1 as (Hiys) "[Hl Hcsort] /=". wp_select; wp_pures; simpl.
-    wp_apply (start_chan_proto_spec N (par_map_protocol IZBs IC (curry red) n ∅));
+    wp_apply (start_chan_proto_spec (par_map_protocol IZBs IC (curry red) n ∅));
       iIntros (cred) "// Hcred".
     { wp_pures. wp_apply (par_map_service_spec with "Hred Hcred"); auto. }
     wp_branch as %_|%Hnil; last first.
diff --git a/theories/examples/sort.v b/theories/examples/sort.v
index b655c01c7d353ed2f9cc487821ea4260c39bce41..5860079210d0e333fd7f3afdbf57d170c865d7df 100644
--- a/theories/examples/sort.v
+++ b/theories/examples/sort.v
@@ -36,7 +36,7 @@ Definition sort_client_func : val := λ: "cmp" "xs",
   recv "c".
 
 Section sort.
-  Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
+  Context `{!heapG Σ, !proto_chanG Σ}.
 
   Definition sort_protocol {A} (I : A → val → iProp Σ) (R : A → A → Prop)
       `{!RelDecision R, !Total R} : iProto Σ :=
@@ -87,9 +87,9 @@ Section sort.
   Lemma sort_service_spec {A} (I : A → val → iProp Σ) (R : A → A → Prop)
       `{!RelDecision R, !Total R} (cmp : val) p c :
     cmp_spec I R cmp -∗
-    {{{ c ↣ iProto_dual (sort_protocol I R) <++> p @ N }}}
+    {{{ c ↣ (iProto_dual (sort_protocol I R) <++> p) }}}
       sort_service cmp c
-    {{{ RET #(); c ↣ p @ N }}}.
+    {{{ RET #(); c ↣ p }}}.
   Proof.
     iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (p c Ψ). wp_lam.
     wp_recv (xs l) as "Hl".
@@ -100,10 +100,10 @@ Section sort.
       wp_send with "[$Hl]"; first by auto. by iApply "HΨ". }
     wp_apply (lsplit_spec with "Hl"); iIntros (l2 vs1 vs2);
       iDestruct 1 as (->) "[Hl1 Hl2]".
-    wp_apply (start_chan_proto_spec N (sort_protocol I R)); iIntros (cy) "Hcy".
+    wp_apply (start_chan_proto_spec (sort_protocol I R)); iIntros (cy) "Hcy".
     { rewrite -{2}(right_id END%proto _ (iProto_dual _)).
       wp_apply ("IH" with "Hcy"); auto. }
-    wp_apply (start_chan_proto_spec N (sort_protocol I R)); iIntros (cz) "Hcz".
+    wp_apply (start_chan_proto_spec (sort_protocol I R)); iIntros (cz) "Hcz".
     { rewrite -{2}(right_id END%proto _ (iProto_dual _)).
       wp_apply ("IH" with "Hcz"); auto. }
     wp_send with "[$Hl1]".
@@ -119,9 +119,9 @@ Section sort.
   Qed.
 
   Lemma sort_service_func_spec p c :
-    {{{ c ↣ iProto_dual sort_protocol_func <++> p @ N }}}
+    {{{ c ↣ (iProto_dual sort_protocol_func <++> p) }}}
       sort_service_func c
-    {{{ RET #(); c ↣ p @ N }}}.
+    {{{ RET #(); c ↣ p }}}.
   Proof.
     iIntros (Ψ) "Hc HΨ". wp_lam.
     wp_recv (A I R ?? cmp) as "#Hcmp".
@@ -136,7 +136,7 @@ Section sort.
     {{{ ys, RET #(); ⌜Sorted R ys⌝ ∗ ⌜ys ≡ₚ xs⌝ ∗ llist I l ys }}}.
   Proof.
     iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
-    wp_apply (start_chan_proto_spec N sort_protocol_func); iIntros (c) "Hc".
+    wp_apply (start_chan_proto_spec sort_protocol_func); iIntros (c) "Hc".
     { rewrite -(right_id END%proto _ (iProto_dual _)).
       wp_apply (sort_service_func_spec with "Hc"); auto. }
     wp_send with "[$Hcmp]".
diff --git a/theories/examples/sort_fg.v b/theories/examples/sort_fg.v
index 248fecd3f4ce254234df32685b4d020dd91c6cb0..50d5bddb99b145a724e9848697e84b009d62ade9 100644
--- a/theories/examples/sort_fg.v
+++ b/theories/examples/sort_fg.v
@@ -52,7 +52,7 @@ Definition sort_service_fg_func : val := λ: "c",
   sort_service_fg "cmp" "c".
 
 Section sort_fg.
-  Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
+  Context `{!heapG Σ, !proto_chanG Σ}.
 
   Section sort_fg_inner.
   Context {A} (I : A → val → iProp Σ) (R : relation A) `{!RelDecision R, !Total R}.
@@ -92,15 +92,15 @@ Section sort_fg.
 
   Lemma sort_service_fg_split_spec c p c1 c2 xs xs1 xs2 :
     {{{
-      c ↣ iProto_dual (sort_fg_head_protocol xs) <++> p @ N ∗
-      c1 ↣ sort_fg_head_protocol xs1 @ N ∗ c2 ↣ sort_fg_head_protocol xs2 @ N
+      c ↣ (iProto_dual (sort_fg_head_protocol xs) <++> p) ∗
+      c1 ↣ sort_fg_head_protocol xs1 ∗ c2 ↣ sort_fg_head_protocol xs2
     }}}
       sort_service_fg_split c c1 c2
     {{{ xs' xs1' xs2', RET #();
       ⌜xs' ≡ₚ xs1' ++ xs2'⌝ ∗
-      c ↣ iProto_dual (sort_fg_tail_protocol (xs ++ xs') []) <++> p @ N ∗
-      c1 ↣ sort_fg_tail_protocol (xs1 ++ xs1') [] @ N ∗
-      c2 ↣ sort_fg_tail_protocol (xs2 ++ xs2') [] @ N
+      c ↣ (iProto_dual (sort_fg_tail_protocol (xs ++ xs') []) <++> p) ∗
+      c1 ↣ sort_fg_tail_protocol (xs1 ++ xs1') [] ∗
+      c2 ↣ sort_fg_tail_protocol (xs2 ++ xs2') []
     }}}.
   Proof.
     iIntros (Ψ) "(Hc & Hc1 & Hc2) HΨ". iLöb as "IH" forall (c c1 c2 xs xs1 xs2 Ψ).
@@ -120,11 +120,11 @@ Section sort_fg.
     Sorted R ys →
     (∀ x, TlRel R x ys' → TlRel R x ys) →
     {{{
-      c ↣ iProto_dual (sort_fg_tail_protocol xs ys) <++> p @ N ∗
-      cin ↣ sort_fg_tail_protocol xs' ys' @ N
+      c ↣ (iProto_dual (sort_fg_tail_protocol xs ys) <++> p) ∗
+      cin ↣ sort_fg_tail_protocol xs' ys'
     }}}
       sort_service_fg_forward c cin
-    {{{ RET #(); c ↣ p @ N ∗ cin ↣ END @ N }}}.
+    {{{ RET #(); c ↣ p ∗ cin ↣ END }}}.
   Proof.
     iIntros (Hxs Hys Hsorted Hrel Ψ) "[Hc Hcin] HΨ".
     iLöb as "IH" forall (c cin xs ys xs' ys' Hxs Hys Hsorted Hrel).
@@ -150,13 +150,13 @@ Section sort_fg.
     (∀ x, TlRel R x ys2 → R x y1 → TlRel R x ys) →
     cmp_spec I R cmp -∗
     {{{
-      c ↣ iProto_dual (sort_fg_tail_protocol xs ys) <++> p @ N ∗
-      c1 ↣ sort_fg_tail_protocol xs1 (ys1 ++ [y1]) @ N ∗
-      c2 ↣ sort_fg_tail_protocol xs2 ys2 @ N ∗
+      c ↣ (iProto_dual (sort_fg_tail_protocol xs ys) <++> p) ∗
+      c1 ↣ sort_fg_tail_protocol xs1 (ys1 ++ [y1]) ∗
+      c2 ↣ sort_fg_tail_protocol xs2 ys2 ∗
       I y1 w1
     }}}
       sort_service_fg_merge cmp c w1 c1 c2
-    {{{ RET #(); c ↣ p @ N }}}.
+    {{{ RET #(); c ↣ p }}}.
   Proof.
     iIntros (Hxs Hys Hsort Htl Htl_le) "#Hcmp !>".
     iIntros (Ψ) "(Hc & Hc1 & Hc2 & HIy1) HΨ".
@@ -193,18 +193,18 @@ Section sort_fg.
 
   Lemma sort_service_fg_spec cmp c p :
     cmp_spec I R cmp -∗
-    {{{ c ↣ iProto_dual sort_fg_protocol <++> p @ N }}}
+    {{{ c ↣ (iProto_dual sort_fg_protocol <++> p) }}}
       sort_service_fg cmp c
-    {{{ RET #(); c ↣ p @ N }}}.
+    {{{ RET #(); c ↣ p }}}.
   Proof.
     iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (c p Ψ).
     wp_rec; wp_pures. wp_branch; wp_pures.
     - wp_recv (x1 v1) as "HIx1". wp_branch; wp_pures.
       + wp_recv (x2 v2) as "HIx2".
-        wp_apply (start_chan_proto_spec N (sort_fg_protocol <++> END)%proto).
+        wp_apply (start_chan_proto_spec (sort_fg_protocol <++> END)%proto).
         { iIntros (cy) "Hcy". wp_apply ("IH" with "Hcy"). auto. }
         iIntros (cy) "Hcy".
-        wp_apply (start_chan_proto_spec N (sort_fg_protocol <++> END)%proto).
+        wp_apply (start_chan_proto_spec (sort_fg_protocol <++> END)%proto).
         { iIntros (cz) "Hcz". wp_apply ("IH" with "Hcz"); auto. }
         iIntros (cz) "Hcz". rewrite !right_id.
         wp_select. wp_send with "[$HIx1]".
@@ -229,9 +229,9 @@ Section sort_fg.
      sort_fg_head_protocol I R [])%proto.
 
   Lemma sort_service_fg_func_spec c p :
-    {{{ c ↣ iProto_dual sort_fg_func_protocol <++> p @ N }}}
+    {{{ c ↣ (iProto_dual sort_fg_func_protocol <++> p) }}}
       sort_service_fg_func c
-    {{{ RET #(); c ↣ p @ N }}}.
+    {{{ RET #(); c ↣ p }}}.
   Proof.
     iIntros (Ψ) "Hc HΨ". wp_lam.
     wp_recv (A I R ? ? cmp) as "#Hcmp".
diff --git a/theories/examples/sort_fg_client.v b/theories/examples/sort_fg_client.v
index 267b7f71ab421038f40b1185030c01ad7f91b631..5eacc5da123b80e925da8720024029d2ba92b20b 100644
--- a/theories/examples/sort_fg_client.v
+++ b/theories/examples/sort_fg_client.v
@@ -23,13 +23,13 @@ Definition sort_client_fg : val := λ: "cmp" "xs",
   recv_all "c" "xs".
 
 Section sort_fg_client.
-  Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
+  Context `{!heapG Σ, !proto_chanG Σ}.
   Context {A} (I : A → val → iProp Σ) (R : relation A) `{!RelDecision R, !Total R}.
 
   Lemma send_all_spec c p xs' l xs :
-    {{{ llist I l xs ∗ c ↣ sort_fg_head_protocol I R xs' <++> p @ N }}}
+    {{{ llist I l xs ∗ c ↣ (sort_fg_head_protocol I R xs' <++> p) }}}
       send_all c #l
-    {{{ RET #(); llist I l [] ∗ c ↣ sort_fg_head_protocol I R (xs' ++ xs) <++> p @ N }}}.
+    {{{ RET #(); llist I l [] ∗ c ↣ (sort_fg_head_protocol I R (xs' ++ xs) <++> p) }}}.
   Proof.
     iIntros (Φ) "[Hl Hc] HΦ".
     iInduction xs as [|x xs] "IH" forall (xs').
@@ -42,10 +42,10 @@ Section sort_fg_client.
 
   Lemma recv_all_spec c p l xs ys' :
     Sorted R ys' →
-    {{{ llist I l [] ∗ c ↣ sort_fg_tail_protocol I R xs ys' <++> p @ N }}}
+    {{{ llist I l [] ∗ c ↣ (sort_fg_tail_protocol I R xs ys' <++> p) }}}
       recv_all c #l
     {{{ ys, RET #();
-        ⌜Sorted R (ys' ++ ys)⌝ ∗ ⌜ys' ++ ys ≡ₚ xs⌝ ∗ llist I l ys ∗ c ↣ p @ N
+        ⌜Sorted R (ys' ++ ys)⌝ ∗ ⌜ys' ++ ys ≡ₚ xs⌝ ∗ llist I l ys ∗ c ↣ p
     }}}.
   Proof.
     iIntros (Hsort Φ) "[Hl Hc] HΦ".
@@ -66,9 +66,9 @@ Section sort_fg_client.
     {{{ ys, RET #(); ⌜Sorted R ys⌝ ∗ ⌜ys ≡ₚ xs⌝ ∗ llist I l ys }}}.
   Proof.
     iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
-    wp_apply (start_chan_proto_spec N (sort_fg_protocol I R <++> END)%proto);
+    wp_apply (start_chan_proto_spec (sort_fg_protocol I R <++> END)%proto);
       iIntros (c) "Hc".
-    { wp_apply (sort_service_fg_spec N with "Hcmp Hc"); auto. }
+    { wp_apply (sort_service_fg_spec with "Hcmp Hc"); auto. }
     wp_apply (send_all_spec with "[$Hl $Hc]"); iIntros "[Hl Hc]".
     wp_select.
     wp_apply (recv_all_spec with "[$Hl $Hc]"); auto.