diff --git a/theories/collections.v b/theories/collections.v
index 007e95e3c12aef028cfb22ca9a8f642fb893507a..2004d072d828736a9b1d0c0de6add78784dd22ea 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -7,11 +7,13 @@ From stdpp Require Export orders list.
 (* FIXME: This file needs a 'Proof Using' hint, but the default we use
    everywhere makes for lots of extra ssumptions. *)
 
-Instance collection_equiv `{ElemOf A C} : Equiv C := λ X Y,
+(* Higher precedence to make sure these instances are not used for other types
+with an [ElemOf] instance, such as lists. *)
+Instance collection_equiv `{ElemOf A C} : Equiv C | 20 := λ X Y,
   ∀ x, x ∈ X ↔ x ∈ Y.
-Instance collection_subseteq `{ElemOf A C} : SubsetEq C := λ X Y,
+Instance collection_subseteq `{ElemOf A C} : SubsetEq C | 20 := λ X Y,
   ∀ x, x ∈ X → x ∈ Y.
-Instance collection_disjoint `{ElemOf A C} : Disjoint C := λ X Y,
+Instance collection_disjoint `{ElemOf A C} : Disjoint C | 20 := λ X Y,
   ∀ x, x ∈ X → x ∈ Y → False.
 Typeclasses Opaque collection_equiv collection_subseteq collection_disjoint.
 
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 121a13ffe16a94be11673bcd1fe488be45357ed8..d53ea3249f4049fdf8bbf37063a8464c3abf6cee 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -80,7 +80,9 @@ Instance map_intersection_with `{Merge M} {A} : IntersectionWith A (M A) :=
 Instance map_difference_with `{Merge M} {A} : DifferenceWith A (M A) :=
   λ f, merge (difference_with f).
 
-Instance map_equiv `{∀ A, Lookup K A (M A), Equiv A} : Equiv (M A) | 18 :=
+(** Higher precedence to make sure it's not used for other types with a [Lookup]
+instance, such as lists. *)
+Instance map_equiv `{∀ A, Lookup K A (M A), Equiv A} : Equiv (M A) | 20 :=
   λ m1 m2, ∀ i, m1 !! i ≡ m2 !! i.
 
 (** The relation [intersection_forall R] on finite maps describes that the