diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 6482abe8610389a39aca43e1d00dcb9d8f6c16a0..6e72e0c062f8c1791e34f0bfb5f927799fa78150 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -111,7 +111,7 @@ Notation "c ↣ p" := (iProto_mapsto c p)
   (at level 20, format "c  ↣  p").
 
 Definition iProto_nchoice {Σ} (a : action) (branches : gmap Z (iProp Σ * iProto Σ)) : iProto Σ :=
-  (<a @ (n : Z)> MSG #n {{fst (branches !!! n)}}; snd (branches !!! n))%proto.
+  (<a @ (n : Z)> MSG #n {{⌜is_Some (branches !! n)⌝ ∗ (branches !!! n).1}}; (branches !!! n).2)%proto.
 
 Definition iProto_choice {Σ} (a : action) (P1 P2 : iProp Σ)
     (p1 p2 : iProto Σ) : iProto Σ :=
@@ -319,27 +319,28 @@ Section channel.
   Qed.
 
   Lemma nselect_spec c (n : Z) branches :
-    {{{ c ↣ iProto_nchoice Send branches ∗ (branches !!! n).1 }}}
+    {{{ c ↣ iProto_nchoice Send branches ∗  ⌜is_Some (branches !! n)⌝ ∗ (branches !!! n).1 }}}
       send c #n
    {{{ RET #(); c ↣ (branches !!! n).2 }}}.
   Proof.
     rewrite /iProto_nchoice. iIntros (Φ) "[Hc HP] HΦ".
     iApply (send_spec with "[Hc HP] HΦ").
     iApply (iProto_mapsto_le with "Hc").
-    iIntros "!>". iExists n. by iFrame "HP".
+    iIntros "!>". iExists n.
+      by iFrame "HP".
   Qed.
 
   Lemma nbranch_spec c branches :
     {{{ c ↣ (iProto_nchoice Recv branches) }}}
       recv c
-    {{{ (n : Z) , RET #n; c ↣ (branches !!! n).2 ∗ (branches !!! n).1 }}}.
+    {{{ (n : Z) , RET #n; c ↣ (branches !!! n).2 ∗ ⌜is_Some (branches !! n)⌝ ∗ (branches !!! n).1 }}}.
   Proof.
     rewrite /iProto_nchoice. iIntros (Φ) "Hc HΦ".
     iApply (recv_spec _ (tele_app _)
-                      (tele_app (TT := [tele _ : Z]) (λ n, (branches !!! n).1))%I
+                      (tele_app (TT := [tele _ : Z]) (λ n, ⌜is_Some (branches !! n)⌝ ∗ (branches !!! n).1))%I
                       (tele_app _) with "[Hc]").
     { iApply (iProto_mapsto_le with "Hc").
-      iIntros "!> /=" (n) "HP". iExists n. by iSplitL. }
+      iIntros "!> /=" (n) "[H1 H2]". iExists n. iSplitL; by auto. }
     rewrite -bi_tforall_forall.
     iIntros "!>" (n) "[Hc H]". iApply "HΦ". iFrame.
   Qed.