diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 0c8c8efaa1ae205fb930a13355afaf005f107d9f..2cc3150ab3c2d8f6562cfdcd35c973af11e6c0f6 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -261,7 +261,7 @@ Lemma map_subset_alt {A} (m1 m2 : M A) :
 Proof.
   rewrite strict_spec_alt. split.
   - intros [? Heq]; split; [done|].
-    destruct (decide (Exists (λ '(i,_), m1 !! i = None) (map_to_list m2)))
+    destruct (decide (Exists (λ ix, m1 !! ix.1 = None) (map_to_list m2)))
       as [[[i x] [?%elem_of_map_to_list ?]]%Exists_exists
          |Hm%(not_Exists_Forall _)]; [eauto|].
     destruct Heq; apply (anti_symm _), map_subseteq_spec; [done|intros i x Hi].