diff --git a/theories/encodings/branching.v b/theories/encodings/branching.v
index f0ce12e13a4beebbd35dacd92563edde24658d97..d94b438f7f0efb73b1924878a170ea9920a2ed03 100644
--- a/theories/encodings/branching.v
+++ b/theories/encodings/branching.v
@@ -57,7 +57,7 @@ Section branching_specs.
       then "b1"
       else "b2".
 
-  Lemma select_st_spec st1 st2 γ c s (b : bool) :
+  Lemma select_st_spec st1 st2 γ c s (b : side) :
     {{{ ⟦ c @ s : st1 <+> st2 ⟧{N,γ} }}}
       select c #s #b
     {{{ RET #(); ⟦ c @ s : (if b then st1 else st2) ⟧{N,γ} }}}.
@@ -68,7 +68,7 @@ Section branching_specs.
     wp_apply (send_st_spec N bool with "[$Hst //]");
     iIntros "Hstl".
     iApply "HΦ".
-    eauto.
+    by destruct b.
   Qed.
 
   Lemma branch_st_spec st1 st2 γ c s (b1 b2 : val) Φ :
diff --git a/theories/examples/branching_proofs.v b/theories/examples/branching_proofs.v
index 5d80c1e16c1d7bd8fb43f1d2cf7bec3fe9f640da..21fb687f599debf7a40312dc8c882e038112a672 100644
--- a/theories/examples/branching_proofs.v
+++ b/theories/examples/branching_proofs.v
@@ -14,14 +14,14 @@ Section BranchingExampleProofs.
     {{{ True }}}
       branch_example b
     {{{ v, RET v; match b with
-                  | true => ⌜v = #5⌝
-                  | false => ⌜v = #()⌝
+                  | Left => ⌜v = #5⌝
+                  | Right => ⌜v = #()⌝
                   end }}}.
   Proof.
     iIntros (Φ H) "HΦ".
     rewrite /branch_example.
     wp_apply (new_chan_st_spec N
-      ((<?> v @ ⌜v = 5⌝, TEnd)  <+> (TEnd)))=> //;
+      ((<?> v @ ⌜v = 5⌝, TEnd) <+> (TEnd)))=> //;
     iIntros (c γ) "[Hstl Hstr]".
     wp_apply (select_st_spec with "Hstl");
     iIntros "Hstl".