diff --git a/theories/logrel/types.v b/theories/logrel/types.v
index 87f351ae3623856985559ae9256f76f0c06ddca9..5d572fb2d60041194581830d86b9ca2373ce26de 100644
--- a/theories/logrel/types.v
+++ b/theories/logrel/types.v
@@ -685,17 +685,18 @@ Section properties.
     Qed.
 
     Definition chanselect : val := λ: "c" "i", send "c" "i";; "c".
-    Lemma ltyped_chanselect Γ (c : val) (i : Z) (Ps : gmap Z (lsty Σ)) :
-      is_Some (Ps !! i) →
+    Lemma ltyped_chanselect Γ (c : val) (i : Z) P Ps :
+      Ps !! i = Some P →
       (Γ ⊨ c : chan (lsty_select Ps)) -∗
-      Γ ⊨ chanselect c #i : chan (Ps !!! i).
+      Γ ⊨ chanselect c #i : chan P.
     Proof.
       iIntros (Hin) "#Hc !>".
       iIntros (vs) "H /=".
       rewrite /chanselect. simpl.
       iDestruct ("Hc" with "H") as "Hc'".
       iMod (wp_value_inv with "Hc'") as "Hc'".
-      wp_send with "[]"=> //.
+      wp_send with "[]"=> //; eauto.
+      rewrite (lookup_total_correct Ps i P)=> //.
       by wp_pures.
     Qed.