diff --git a/theories/encodings/branching.v b/theories/encodings/branching.v
index 44a0eb43b588bad2b8be558e4a6e6b8992bfd295..4bdf43c9aa4bb5f8caeeec8b03393ff4f0211807 100644
--- a/theories/encodings/branching.v
+++ b/theories/encodings/branching.v
@@ -90,4 +90,8 @@ Section branching_specs.
     - wp_pures. iApply ("HΦ'"). eauto with iFrame.
   Qed.
 
-End branching_specs.
\ No newline at end of file
+End branching_specs.
+
+Notation "'branch:' c @ s 'left' e1 'right' e2" :=
+  (branch c s (λ: <>, e1)%E (λ: <>, e2)%E #())
+    (at level 200, c, s, e1, e2 at level 200) : expr_scope.
diff --git a/theories/examples/branching_examples.v b/theories/examples/branching_examples.v
index 327ecfdc5ec2114532d048b971ef85df00207b1a..bd75583c951a3c6362853ab6f216bb0e47b59c7b 100644
--- a/theories/examples/branching_examples.v
+++ b/theories/examples/branching_examples.v
@@ -11,9 +11,9 @@ Section BranchingExamples.
   Definition branch_example b : expr :=
     (let: "c" := new_chan #() in
      select "c" #Left #b;;
-     Fork((branch "c" #Right
-      (λ: <>, send "c" #Right #5)
-      (λ: <>, #())) #());;
+     Fork(branch: "c" @ #Right
+      left  send "c" #Right #5
+      right #());;
      (if: #b then recv "c" #Left else #()))%E.
 
 End BranchingExamples.
\ No newline at end of file