diff --git a/theories/utils/switch.v b/theories/utils/switch.v
index 1e2d61e6aa5fc48505a29d32371c9fb91389af8a..f4b820ae1d14787a210e29ff548e7ddf88ad5fa8 100644
--- a/theories/utils/switch.v
+++ b/theories/utils/switch.v
@@ -36,7 +36,7 @@ Proof.
 Qed.
 
 Lemma lookup_map_string_seq_None {A} y j z (vs : list A) :
-  (∀ i, y +:+ pretty i ≠ z) →
+  (∀ i : nat, y +:+ pretty i ≠ z) →
   map_string_seq y j vs !! z = None.
 Proof.
   intros. revert j. induction vs as [|v vs IH]=> j //=.