diff --git a/theories/list.v b/theories/list.v
index 0e220fd345fecdcf652ff70d99c144da4043c769..98c9d5ee0a1329cc96fcd17b3de2160a17f365d6 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -4,6 +4,14 @@ From Coq Require Export Permutation.
 From stdpp Require Export numbers base option.
 From stdpp Require Import options.
 
+(** FIXME: Workaround for https://github.com/coq/coq/issues/14571 *)
+(** 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*".