diff --git a/theories/channel/proto_channel.v b/theories/channel/proto_channel.v
index f39f009f71b8e53cb0115eeea0714359ffede48c..3d7940207f7eab317533b5214468c6150bc4579f 100644
--- a/theories/channel/proto_channel.v
+++ b/theories/channel/proto_channel.v
@@ -7,6 +7,10 @@ From osiris.utils Require Import auth_excl.
 Set Default Proof Using "Type*".
 Export action.
 
+Definition start_chan : val := λ: "f",
+  let: "cc" := new_chan #() in
+  Fork ("f" (Snd "cc"));; Fst "cc".
+
 (** Camera setup *)
 Class proto_chanG Σ := {
   proto_chanG_chanG :> chanG Σ;
@@ -655,6 +659,18 @@ Section proto.
     iApply "HΨ". by iFrame.
   Qed.
 
+  Lemma start_chan_proto_spec p Ψ (f : val) :
+    ▷ (∀ c, c ↣ iProto_dual p @ N -∗ WP f c {{ _, True }}) -∗
+    ▷ (∀ c, c ↣ p @ N -∗ Ψ c) -∗
+    WP start_chan f {{ Ψ }}.
+  Proof.
+    iIntros "Hfork HΨ". wp_lam.
+    wp_apply (new_chan_proto_spec p with "[//]"); iIntros (c1 c2) "[Hc1 Hc2]".
+    wp_apply (wp_fork with "[Hfork Hc2]").
+    { iNext. wp_apply ("Hfork" with "Hc2"). }
+    wp_pures. iApply ("HΨ" with "Hc1").
+  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 }}}
       send c (pc x).1.1
diff --git a/theories/examples/list_sort.v b/theories/examples/list_sort.v
index 30bcafd746c1b3a9afa24d46527ba6774587dd85..805de1bc592d103ca68e690712ead1b4e5826502 100644
--- a/theories/examples/list_sort.v
+++ b/theories/examples/list_sort.v
@@ -16,7 +16,7 @@ Definition lmerge : val :=
       | SOME "_" =>
         let: "y" := lhead "hys" in
         let: "z" := lhead "hzs" in
-        if: ("cmp" "y" "z")
+        if: "cmp" "y" "z"
         then lcons "y" ("go" "cmp" (ltail "hys") "hzs")
         else lcons "z" ("go" "cmp" "hys" (ltail "hzs"))
       end
@@ -31,14 +31,11 @@ Definition list_sort_service : val :=
     let: "ys_zs" := lsplit !"xs" in
     let: "ys" := ref (Fst "ys_zs") in
     let: "zs" := ref (Snd "ys_zs") in
-    let: "cy" := new_chan #() in Fork("go" (Snd "cy"));;
-    let: "cz" := new_chan #() in Fork("go" (Snd "cz"));;
-    send (Fst "cy") "cmp";;
-    send (Fst "cy") "ys";;
-    send (Fst "cz") "cmp";;
-    send (Fst "cz") "zs";;
-    recv (Fst "cy");;
-    recv (Fst "cz");;
+    let: "cy" := start_chan "go" in
+    let: "cz" := start_chan "go" in
+    send "cy" "cmp";; send "cy" "ys";;
+    send "cz" "cmp";; send "cz" "zs";;
+    recv "cy";; recv "cz";;
     "xs" <- lmerge "cmp" !"ys" !"zs";;
     send "c" #().
 
@@ -46,23 +43,17 @@ Definition loop_sort_service_go : val :=
   rec: "go" "c" :=
     if: recv "c" then list_sort_service "c";; "go" "c"
     else if: recv "c" then
-      let: "d" := new_chan #() in
-      Fork ("go" (Snd "d"));;
-      send "c" (Fst "d");;
+      let: "d" := start_chan "go" in
+      send "c" "d";;
       "go" "c"
     else #().
 Definition loop_sort_service : val := λ: <>,
-  let: "c" := new_chan #() in
-  Fork (loop_sort_service_go (Snd "c"));;
-  Fst "c".
+  start_chan loop_sort_service_go.
 
 Definition list_sort_client : val := λ: "cmp" "xs",
-  let: "c" := new_chan #() in
-  Fork (list_sort_service (Snd "c"));;
-  send (Fst "c") "cmp";;
-  send (Fst "c") "xs";;
-  recv (Fst "c");;
-  #().
+  let: "c" := start_chan list_sort_service in
+  send "c" "cmp";; send "c" "xs";;
+  recv "c".
 
 Section list_sort.
   Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
@@ -139,27 +130,23 @@ Section list_sort.
     wp_load. wp_apply (lsplit_spec (A:=val) with "[//]"); iIntros (vs1 vs2 <-).
     wp_alloc l1 as "Hl1"; wp_alloc l2 as "Hl2".
     iDestruct (big_sepL2_app_inv_r with "HI") as (xs1 xs2 ->) "[HI1 HI2]".
-    wp_apply (new_chan_proto_spec N sort_protocol)=> //.
-    iIntros (cy1 cy2) "[Hcy1 Hcy2]".
-    wp_apply (wp_fork with "[Hcy2]").
-    { iNext. rewrite -{2}(right_id END%proto _ (iProto_dual _)).
-      wp_apply ("IH" with "Hcy2"); auto. }
-    wp_apply (new_chan_proto_spec N sort_protocol)=> //.
-    iIntros (cz1 cz2) "[Hcz1 Hcz2]".
-    wp_apply (wp_fork with "[Hcz2]").
-    { iNext. rewrite -{2}(right_id END%proto _ (iProto_dual _)).
-      wp_apply ("IH" with "Hcz2"); auto. }
-    wp_apply (send_proto_spec with "Hcy1"); simpl.
-    iExists _, I, R, _, _, cmp. iSplit; first done. iIntros "{$Hcmp} !> Hcy1".
-    wp_apply (send_proto_spec with "Hcy1"); simpl.
-    iExists xs1, l1, vs1. iSplit; first done. iIntros "{$Hl1 $HI1} !> Hcy1".
-    wp_apply (send_proto_spec with "Hcz1"); simpl.
-    iExists _, I, R, _, _, cmp. iSplit; first done. iIntros "{$Hcmp} !> Hcz1".
-    wp_apply (send_proto_spec with "Hcz1"); simpl.
-    iExists xs2, l2, vs2. iSplit; first done. iIntros "{$Hl2 $HI2} !> Hcz1".
-    wp_apply (recv_proto_spec with "Hcy1"); simpl.
+    wp_apply (start_chan_proto_spec N sort_protocol); 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); iIntros (cz) "Hcz".
+    { rewrite -{2}(right_id END%proto _ (iProto_dual _)).
+      wp_apply ("IH" with "Hcz"); auto. }
+    wp_apply (send_proto_spec with "Hcy"); simpl.
+    iExists _, I, R, _, _, cmp. iSplit; first done. iIntros "{$Hcmp} !> Hcy".
+    wp_apply (send_proto_spec with "Hcy"); simpl.
+    iExists xs1, l1, vs1. iSplit; first done. iIntros "{$Hl1 $HI1} !> Hcy".
+    wp_apply (send_proto_spec with "Hcz"); simpl.
+    iExists _, I, R, _, _, cmp. iSplit; first done. iIntros "{$Hcmp} !> Hcz".
+    wp_apply (send_proto_spec with "Hcz"); simpl.
+    iExists xs2, l2, vs2. iSplit; first done. iIntros "{$Hl2 $HI2} !> Hcz".
+    wp_apply (recv_proto_spec with "Hcy"); simpl.
     iIntros (ys1 ws1) "_". iDestruct 1 as (??) "[Hl1 HI1]".
-    wp_apply (recv_proto_spec with "Hcz1"); simpl.
+    wp_apply (recv_proto_spec with "Hcz"); simpl.
     iIntros (ys2 ws2) "_". iDestruct 1 as (??) "[Hl2 HI2]".
     do 2 wp_load.
     wp_apply (lmerge_spec with "Hcmp [$HI1 $HI2]"). iIntros (ws) "HI".
@@ -195,12 +182,10 @@ Section list_sort.
     { wp_apply (list_sort_service_spec with "Hc"); iIntros "Hc".
       by wp_apply ("IH" with "Hc"). }
     wp_apply (branch_spec with "Hc"); iIntros ([]) "/= Hc"; wp_if.
-    - wp_apply (new_chan_proto_spec N loop_sort_protocol with "[//]");
-        iIntros (d1 d2) "[Hd1 Hd2]".
-      wp_apply (wp_fork with "[Hd2]").
-      { iNext. wp_apply ("IH" with "Hd2"); auto. }
+    - wp_apply (start_chan_proto_spec N loop_sort_protocol); iIntros (d) "Hd".
+      { wp_apply ("IH" with "Hd"); auto. }
       wp_apply (send_proto_spec with "Hc"); simpl.
-      iExists d1; iSplit; first done. iIntros "{$Hd1} !> Hc".
+      iExists d; iSplit; first done. iIntros "{$Hd} !> Hc".
       by wp_apply ("IH" with "Hc").
     - by iApply "HΨ".
   Qed.
@@ -213,25 +198,21 @@ Section list_sort.
     {{{ ys ws, RET #(); ⌜Sorted R ys⌝ ∗ ⌜ys ≡ₚ xs⌝ ∗
                l ↦ val_encode ws ∗ [∗ list] y;w ∈ ys;ws, I y w }}}.
   Proof.
-    iIntros "#Hcmp !>" (Φ) "Hl HΦ".
-    wp_lam.
-    wp_apply (new_chan_proto_spec N (sort_protocol <++> END)%proto with "[//]")=> /=.
-    iIntros (c c') "[Hstl Hstr]".
-    wp_apply (wp_fork with "[Hstr]").
-    { iNext.
-      rewrite (iProto_dual_app sort_protocol (END%proto)).
-      wp_apply (list_sort_service_spec (END%proto) c' with "Hstr"); auto. }
-    wp_apply (send_proto_spec with "Hstl"); simpl.
+    iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
+    wp_apply (start_chan_proto_spec N sort_protocol); iIntros (c) "Hc".
+    { rewrite -(right_id END%proto _ (iProto_dual _)).
+      wp_apply (list_sort_service_spec with "Hc"); auto. }
+    wp_apply (send_proto_spec with "Hc"); simpl.
     iExists _, I, R, _, _, cmp.
     iSplitR=> //.
     iSplitR=> //.
-    iIntros "!> Hstl".
-    wp_apply (send_proto_spec with "Hstl"); simpl.
+    iIntros "!> Hc".
+    wp_apply (send_proto_spec with "Hc"); simpl.
     iExists xs, l, vs.
     iSplitR=> //.
-    iIntros "{$Hl} !> Hstl".
-    wp_apply (recv_proto_spec with "Hstl"); simpl.
-    iIntros (ys ws) "Hstl (Hsorted & Hperm & Hl & HI)".
+    iIntros "{$Hl} !> Hc".
+    wp_apply (recv_proto_spec with "Hc"); simpl.
+    iIntros (ys ws) "Hc (Hsorted & Hperm & Hl & HI)".
     wp_pures. iApply "HΦ". iFrame.
   Qed.