diff --git a/theories/list.v b/theories/list.v
index 80e43e1a33713569cf3c2fd460ab55771c8ede6c..98c9d5ee0a1329cc96fcd17b3de2160a17f365d6 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -5,11 +5,12 @@ From stdpp Require Export numbers base option.
 From stdpp Require Import options.
 
 (** FIXME: Workaround for https://github.com/coq/coq/issues/14571 *)
-(** Remove the instance [Permutation_app'], since its priority is 10, which is
-above the priority 5 of [proper_relation], and add it back with the right
-priority (default = 0, since the instance has no premises). *)
-Global Remove Hints Permutation_app' : typeclass_instances.
-Global Existing Instance Permutation_app'.
+(** Remove the instances [Permutation_cons] and [Permutation_app'] since their
+priorities are 10, which is above the priority 5 of [proper_relation], and add
+them back with the right priority (default = 0, since these instances have no
+premises). *)
+Global Remove Hints Permutation_cons Permutation_app' : typeclass_instances.
+Global Existing Instances Permutation_cons Permutation_app'.
 
 (* Pick up extra assumptions from section parameters. *)
 Set Default Proof Using "Type*".