diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
new file mode 100644
index 0000000000000000000000000000000000000000..42da27262468f499d06223ab30775229e6a7e96b
--- /dev/null
+++ b/theories/channel/proofmode.v
@@ -0,0 +1,277 @@
+From iris.heap_lang Require Export proofmode notation.
+From iris.proofmode Require Export tactics.
+From osiris Require Export proto_channel.
+From iris.proofmode Require Import coq_tactics reduction spec_patterns.
+
+(* TODO: strip laters *)
+Lemma tac_wp_recv `{!proto_chanG Σ, !heapG Σ} {TT : tele} Δ i j K N
+    c p (pc : TT → val * iProp Σ * iProto Σ) Φ :
+  envs_lookup i Δ = Some (false, c ↣ p @ N)%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
+    | Some Δ'' => envs_entails Δ'' (WP fill K (of_val (pc x).1.1) {{ Φ }})
+    | None => False
+    end) →
+  envs_entails Δ (WP fill K (recv c) {{ Φ }}).
+Proof.
+  rewrite envs_entails_eq /ProtoNormalize /= tforall_forall right_id=> ? Hp HΦ.
+  rewrite envs_lookup_sound //; simpl. rewrite -Hp.
+  rewrite -wp_bind. eapply bi.wand_apply; [by eapply recv_proto_spec|f_equiv].
+  rewrite -bi.later_intro bi_tforall_forall; apply bi.forall_intro=> x.
+  specialize (HΦ x). destruct (envs_app _ _) as [Δ'|] eqn:HΔ'=> //.
+  rewrite envs_app_sound //; simpl.
+  by rewrite right_id HΦ bi.wand_curry.
+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
+    iAssumptionCore || fail "wp_recv: cannot find" c "↣ ? @ ?" in
+  wp_pures;
+  let Hnew := iFresh in
+  lazymatch goal with
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_recv _ _ Hnew K))
+      |fail 1 "wp_recv: cannot find 'recv' in" e];
+    [solve_mapsto ()
+       |iSolveTC || fail 1 "wp_send: protocol not of the shape <?>"
+    |pm_reduce; simpl; tac_intros;
+     tac Hnew;
+     wp_finish]
+  | _ => fail "wp_recv: not a 'wp'"
+  end.
+
+Tactic Notation "wp_recv" "(" intropattern_list(xs) ")" "as" constr(pat) :=
+  wp_recv_core (intros xs) as (fun H => iDestructHyp H as pat).
+Tactic Notation "wp_recv" "(" 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" "(" 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" "(" 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" "(" 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" "(" 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" "(" 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" "(" 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" "(" 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).
+
+Lemma tac_wp_send `{!proto_chanG Σ, !heapG Σ} {TT : tele} Δ neg i js K N
+    c v p (pc : TT → val * iProp Σ * iProto Σ) Φ :
+  envs_lookup i Δ = Some (false, c ↣ p @ N)%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
+       | Some Δ2' =>
+          v = (pc x).1.1 ∧
+          envs_entails Δ1 (pc x).1.2 ∧
+          envs_entails Δ2' (WP fill K (of_val #()) {{ Φ }})
+       | None => False
+       end
+    | None => False
+    end) →
+  envs_entails Δ (WP fill K (send c v) {{ Φ }}).
+Proof.
+  rewrite envs_entails_eq /ProtoNormalize /= right_id texist_exist=> ? Hp [x HΦ].
+  rewrite envs_lookup_sound //; simpl. rewrite -Hp.
+  rewrite -wp_bind. eapply bi.wand_apply; [by eapply send_proto_spec|f_equiv].
+  rewrite bi_texist_exist -(bi.exist_intro x).
+  destruct (envs_split _ _ _) as [[Δ1 Δ2]|] eqn:? => //.
+  destruct (envs_app _ _ _) as [Δ2'|] eqn:? => //.
+  rewrite envs_split_sound //; rewrite (envs_app_sound Δ2) //; simpl.
+  destruct HΦ as (-> & -> & ->). rewrite bi.pure_True // left_id.
+  by rewrite -bi.later_intro right_id.
+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
+    iAssumptionCore || fail "wp_send: cannot find" c "↣ ? @ ?" in
+  let solve_done d :=
+    lazymatch d with
+    | true =>
+       done ||
+       let Q := match goal with |- envs_entails _ ?Q => Q end in
+       fail "wp_send: cannot solve" Q "using done"
+    | false => idtac
+    end in
+  lazymatch spec_pat.parse pat with
+  | [SGoal (SpecGoal GSpatial ?neg ?Hs_frame ?Hs ?d)] =>
+     let Hs' := eval cbv in (if neg then Hs else Hs_frame ++ Hs) in
+     wp_pures;
+     lazymatch goal with
+     | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+       first
+         [reshape_expr e ltac:(fun K e' => eapply (tac_wp_send _ neg _ Hs' K))
+         |fail 1 "wp_send: cannot find 'send' in" e];
+       [solve_mapsto ()
+       |iSolveTC || fail 1 "wp_send: protocol not of the shape <!>"
+       |pm_reduce; simpl; tac_exist;
+        repeat lazymatch goal with
+        | |- ∃ _, _ => eexists _
+        end;
+        lazymatch goal with
+        | |- False => fail "wp_send:" Hs' "not fresh"
+        | _ => split; [try fast_done|split;[iFrame Hs_frame; solve_done d|wp_finish]]
+        end]
+     | _ => fail "wp_send: not a 'wp'"
+     end
+  | _ => fail "wp_send: only a single goal spec pattern supported"
+  end.
+
+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.
+
+Lemma tac_wp_branch `{!proto_chanG Σ, !heapG Σ} Δ i j K N
+    c p P1 P2 (p1 p2 : iProto Σ) Φ :
+  envs_lookup i Δ = Some (false, c ↣ p @ N)%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
+    | Some Δ'' => envs_entails Δ'' (WP fill K (of_val #b) {{ Φ }})
+    | None => False
+    end) →
+  envs_entails Δ (WP fill K (recv c) {{ Φ }}).
+Proof.
+  rewrite envs_entails_eq /ProtoNormalize /= right_id=> ? Hp HΦ.
+  rewrite envs_lookup_sound //; simpl. rewrite -Hp.
+  rewrite -wp_bind. eapply bi.wand_apply; [by eapply branch_spec|f_equiv].
+  rewrite -bi.later_intro; apply bi.forall_intro=> b.
+  specialize (HΦ b). destruct (envs_app _ _) as [Δ'|] eqn:HΔ'=> //.
+  rewrite envs_app_sound //; simpl. by rewrite right_id HΦ.
+Qed.
+
+Tactic Notation "wp_branch" "as" constr(pat1) constr(pat2) :=
+  let solve_mapsto _ :=
+    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
+  lazymatch goal with
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_branch _ _ Hnew K))
+      |fail 1 "wp_branch: cannot find 'recv' in" e];
+    [solve_mapsto ()
+       |iSolveTC || fail 1 "wp_send: protocol not of the shape <&>"
+    |pm_reduce; intros [];
+       [iDestructHyp Hnew as pat1|iDestructHyp Hnew as pat2]; wp_finish]
+  | _ => fail "wp_branch: not a 'wp'"
+  end.
+
+Tactic Notation "wp_branch" := wp_branch as "_" "_".
+
+Lemma tac_wp_select `{!proto_chanG Σ, !heapG Σ} Δ neg i js K N
+    c (b : bool) p P1 P2 (p1 p2 : iProto Σ) Φ :
+  envs_lookup i Δ = Some (false, c ↣ p @ N)%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
+     | Some Δ2' =>
+        envs_entails Δ1 (if b then P1 else P2) ∧
+        envs_entails Δ2' (WP fill K (of_val #()) {{ Φ }})
+     | None => False
+     end
+  | None => False
+  end →
+  envs_entails Δ (WP fill K (send c #b) {{ Φ }}).
+Proof.
+  rewrite envs_entails_eq /ProtoNormalize /= right_id=> ? Hp HΦ.
+  rewrite envs_lookup_sound //; simpl. rewrite -Hp.
+  rewrite -wp_bind. eapply bi.wand_apply; [by eapply select_spec|].
+  rewrite -assoc; f_equiv.
+  destruct (envs_split _ _ _) as [[Δ1 Δ2]|] eqn:? => //.
+  destruct (envs_app _ _ _) as [Δ2'|] eqn:? => //.
+  rewrite envs_split_sound //; rewrite (envs_app_sound Δ2) //; simpl.
+  destruct HΦ as [-> ->]. by rewrite -bi.later_intro right_id.
+Qed.
+
+Tactic Notation "wp_select" "with" constr(pat) :=
+  let solve_mapsto _ :=
+    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
+    | true =>
+       done ||
+       let Q := match goal with |- envs_entails _ ?Q => Q end in
+       fail "wp_select: cannot solve" Q "using done"
+    | false => idtac
+    end in
+  lazymatch spec_pat.parse pat with
+  | [SGoal (SpecGoal GSpatial ?neg ?Hs_frame ?Hs ?d)] =>
+     let Hs' := eval cbv in (if neg then Hs else Hs_frame ++ Hs) in
+     wp_pures;
+     lazymatch goal with
+     | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+       first
+         [reshape_expr e ltac:(fun K e' => eapply (tac_wp_select _ neg _ Hs' K))
+         |fail 1 "wp_select: cannot find 'send' in" e];
+       [solve_mapsto ()
+       |iSolveTC || fail 1 "wp_select: protocol not of the shape <+>"
+       |pm_reduce;
+        lazymatch goal with
+        | |- False => fail "wp_select:" Hs' "not fresh"
+        | _ => split;[iFrame Hs_frame; solve_done d|wp_finish]
+        end]
+     | _ => fail "wp_select: not a 'wp'"
+     end
+  | _ => fail "wp_select: only a single goal spec pattern supported"
+  end.
+
+Tactic Notation "wp_select" := wp_select with "[//]".
diff --git a/theories/examples/list_sort.v b/theories/examples/list_sort.v
index bfb1d34ea08d18f1a5dd09f7e4aa8cd38be07275..aef3c25815590129458ece8c4b0850c6f2cc3e5f 100644
--- a/theories/examples/list_sort.v
+++ b/theories/examples/list_sort.v
@@ -89,8 +89,8 @@ Section list_sort.
   Proof.
     iIntros (Ψ) "Hc HΨ". iLöb as "IH" forall (p c Ψ).
     wp_lam.
-    wp_recv (A I R ?? cmp) with "#Hcmp".
-    wp_recv (xs l vs) with "[Hl HI]".
+    wp_recv (A I R ?? cmp) as "#Hcmp".
+    wp_recv (xs l vs) as "[Hl HI]".
     wp_load. wp_apply (llength_spec (A:=val) with "[//]"); iIntros (_).
     iDestruct (big_sepL2_length with "HI") as %<-.
     wp_op; case_bool_decide as Hlen; wp_if.
@@ -110,8 +110,8 @@ Section list_sort.
     wp_send with "[$Hl1 $HI1]".
     wp_send with "[$Hcmp]".
     wp_send with "[$Hl2 $HI2]".
-    wp_recv (ys1 ws1) with (??) "[Hl1 HI1]".
-    wp_recv (ys2 ws2) with (??) "[Hl2 HI2]".
+    wp_recv (ys1 ws1) as (??) "[Hl1 HI1]".
+    wp_recv (ys2 ws2) as (??) "[Hl2 HI2]".
     do 2 wp_load.
     wp_apply (lmerge_spec with "Hcmp [$HI1 $HI2]"). iIntros (ws) "HI".
     wp_store.
@@ -136,7 +136,7 @@ Section list_sort.
       wp_apply (list_sort_service_spec with "Hc"); auto. }
     wp_send with "[$Hcmp]".
     wp_send with "[$Hl]".
-    wp_recv (ys ws) with "(Hsorted & Hperm & Hl & HI)".
+    wp_recv (ys ws) as "(Hsorted & Hperm & Hl & HI)".
     wp_pures. iApply "HΦ"; iFrame.
   Qed.
 End list_sort.
diff --git a/theories/examples/list_sort_elem.v b/theories/examples/list_sort_elem.v
index 6534b35e9c5decdb509fab80af64659621ee1583..3152d73775aa46da8f1863db572a80f03f391d00 100644
--- a/theories/examples/list_sort_elem.v
+++ b/theories/examples/list_sort_elem.v
@@ -92,16 +92,13 @@ Section list_sort_elem.
     }}}.
   Proof.
     iIntros (Ψ) "(Hc & Hc1 & Hc2) HΨ". iLöb as "IH" forall (c c1 c2 xs xs1 xs2 Ψ).
-    wp_rec. wp_apply (branch_spec with "Hc"); iIntros ([]) "[Hc _]"; wp_pures.
-    - wp_recv (x v) with "HI".
-      wp_apply (select_spec with "[$Hc1]")=> //=; iIntros "Hc1".
-      wp_send with "[$HI]".
+    wp_rec. wp_branch; wp_pures.
+    - wp_recv (x v) as "HI". wp_select. wp_send with "[$HI]".
       wp_apply ("IH" with "Hc Hc2 Hc1").
       iIntros (xs' xs1' xs2'); iDestruct 1 as (Hxs') "(Hc & Hc2 & Hc1)".
       rewrite -!(assoc_L (++)).
       iApply "HΨ". iFrame "Hc Hc1 Hc2". by rewrite Hxs' (comm (++) xs1') assoc_L.
-    - wp_apply (select_spec with "[$Hc1]")=> //=; iIntros "Hc1".
-      wp_apply (select_spec with "[$Hc2]")=> //=; iIntros "Hc2".
+    - wp_select. wp_select.
       iApply ("HΨ" $! [] [] []). rewrite !right_id_L. by iFrame.
   Qed.
 
@@ -119,19 +116,18 @@ Section list_sort_elem.
   Proof.
     iIntros (Hxs Hys Hsorted Hrel Ψ) "[Hc Hcin] HΨ".
     iLöb as "IH" forall (c cin xs ys xs' ys' Hxs Hys Hsorted Hrel).
-    wp_rec. wp_apply (branch_spec with "Hcin"); iIntros ([]) "[Hcin Hys']".
-    - iClear "Hys'". wp_recv (x v) with (Htl) "HI".
-      wp_apply (select_spec with "[$Hc]")=> //=; iIntros "Hc".
-      wp_send with "[$HI]"; first by auto.
+    wp_rec. wp_branch as "_" "Hys'".
+    - wp_recv (x v) as (Htl) "HI".
+      wp_select. wp_send with "[$HI]"; first by auto.
       wp_apply ("IH" with "[%] [%] [%] [%] Hc Hcin HΨ").
       { done. }
       { by rewrite Hys -!assoc_L (comm _ zs). }
       { rewrite fmap_app /=. apply Sorted_snoc; auto. }
       { intros x'. rewrite !fmap_app.
         inversion 1; discriminate_list || simplify_list_eq. by constructor. }
-    - iDestruct "Hys'" as %Hys'. wp_apply (select_spec with "[$Hc]")=> //=.
-      { by rewrite Hys Hxs Hys'. }
-      iIntros "Hc". iApply "HΨ". iFrame.
+    - iDestruct "Hys'" as %Hys'. wp_select with "[]".
+      { by rewrite /= Hys Hxs Hys'. }
+      iApply "HΨ". iFrame.
   Qed.
 
   Lemma list_sort_elem_service_merge_spec cmp c c1 c2 xs ys xs1 xs2 y1 w1 ys1 ys2 :
@@ -152,13 +148,11 @@ Section list_sort_elem.
     iIntros (Hxs Hys Hsort Htl Htl_le) "#Hcmp !>".
     iIntros (Ψ) "(Hc & Hc1 & Hc2 & HIy1) HΨ".
     iLöb as "IH" forall (c1 c2 xs1 xs2 ys y1 w1 ys1 ys2 Hxs Hys Hsort Htl Htl_le).
-    wp_rec. wp_apply (branch_spec with "[$Hc2]"); iIntros ([]) "[Hc2 Hys2]".
-    - iClear "Hys2".
-      wp_recv (x v) with (Htl2) "HIx".
+    wp_rec. wp_branch as "_" "Hys2".
+    - wp_recv (x v) as (Htl2) "HIx".
       wp_pures. wp_apply ("Hcmp" with "[$HIy1 $HIx]"); iIntros "[HIy1 HIx]".
       case_bool_decide.
-      + wp_apply (select_spec with "[$Hc]")=> //=; iIntros "Hc".
-        wp_send with "[$HIy1 //]".
+      + wp_select. wp_send with "[$HIy1 //]".
         wp_apply ("IH" with "[%] [%] [%] [%] [%] Hc Hc2 Hc1 HIx").
         { by rewrite comm. }
         { by rewrite assoc (comm _ ys2) Hys. }
@@ -167,8 +161,7 @@ Section list_sort_elem.
         { intros x'. rewrite !fmap_app.
           inversion 1; discriminate_list || simplify_list_eq. by constructor. }
         iIntros "(?&?&?)". iApply "HΨ"; iFrame.
-      + wp_apply (select_spec with "[$Hc]")=> //=; iIntros "Hc".
-        wp_send with "[$HIx]".
+      + wp_select. wp_send with "[$HIx]".
         { iPureIntro. by apply Htl_le, total_not. }
         wp_apply ("IH" with "[% //] [%] [%] [%] [%] Hc Hc1 Hc2 HIy1 HΨ").
         { by rewrite Hys assoc. }
@@ -177,8 +170,7 @@ Section list_sort_elem.
         { intros x'. rewrite !fmap_app.
           inversion 1; discriminate_list || simplify_list_eq. by constructor. }
     - iDestruct "Hys2" as %Hys2.
-      wp_apply (select_spec with "[$Hc]")=> //=; iIntros "Hc".
-      wp_send with "[$HIy1 //]".
+      wp_select. wp_send with "[$HIy1 //]".
       wp_apply (list_sort_elem_service_move_spec with "[$Hc $Hc1]").
       { done. }
       { by rewrite Hys Hys2 -!assoc_L (comm _ xs2). }
@@ -195,34 +187,27 @@ Section list_sort_elem.
     {{{ RET #(); c ↣ END @ N }}}.
   Proof.
     iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (c Ψ).
-    wp_rec; wp_pures.
-    wp_apply (branch_spec with "Hc"); iIntros ([]) "[Hc _]"; wp_pures.
-    - wp_recv (x1 v1) with "HIx1".
-      wp_apply (branch_spec with "Hc"); iIntros ([]) "[Hc _]"; wp_pures.
-      + wp_recv (x2 v2) with "HIx2".
+    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 list_sort_elem_protocol).
         { iIntros (cy) "Hcy". wp_apply ("IH" with "Hcy"); auto. }
         iIntros (cy) "Hcy".
         wp_apply (start_chan_proto_spec N list_sort_elem_protocol).
         { iIntros (cz) "Hcz". wp_apply ("IH" with "Hcz"); auto. }
         iIntros (cz) "Hcz".
-        wp_apply (select_spec with "[$Hcy]")=> //; iIntros "Hcy".
-        wp_send with "[$HIx1]".
-        wp_apply (select_spec with "[$Hcz]")=> //; iIntros "Hcz".
-        wp_send with "[$HIx2]".
+        wp_select. wp_send with "[$HIx1]".
+        wp_select. wp_send with "[$HIx2]".
         wp_apply (list_sort_elem_service_split_spec with "[$Hc $Hcy $Hcz]").
         iIntros (xs' xs1' xs2'); iDestruct 1 as (Hxs') "(Hc & Hcy & Hcz) /=".
-        wp_apply (branch_spec with "Hcy"); iIntros (b) "[Hcy Hnil]".
-        destruct b; last first.
+        wp_branch as "_" "Hnil"; last first.
         { by iDestruct "Hnil" as %?%Permutation_nil_cons. }
-        iClear "Hnil".
-        wp_recv (x v) with "[_ HIx]".
+        wp_recv (x v) as "[_ HIx]".
         wp_apply (list_sort_elem_service_merge_spec _ _ _ _ _ [] _ _ _ _ [] []
           with "Hcmp [$Hc $Hcy $Hcz $HIx]"); simpl; auto using TlRel_nil, Sorted_nil.
         { by rewrite Hxs' Permutation_middle. }
         iIntros "(Hc & Hcy & Hcz)". by iApply "HΨ".
-      + wp_apply (select_spec with "[$Hc]")=> //=; iIntros "Hc".
-        wp_send with "[$HIx1]"; first by auto using TlRel_nil.
+      + wp_select. wp_send with "[$HIx1]"; first by auto using TlRel_nil.
         by wp_apply (select_spec with "[$Hc]").
     - by wp_apply (select_spec with "[$Hc]").
   Qed.