diff --git a/theories/base.v b/theories/base.v
index c4b2df78ec3fa3379ed135f5865d1fcc9c68dca3..77abf35f7f0a151eadaa78dad2e1c973cd8fe4f6 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -256,7 +256,7 @@ of shape [Proper (eq ==> ?R) f] using [Proper (eq ==> (equiv (A:=A))) f]
 when an equivalence relation is available on type [A]. We put this instance
 at level 150 so it does not take precedence over Coq's stdlib instances,
 favoring inference of [eq] (all Coq functions are automatically morphisms
-for [eq]). *)
+for [eq]). We have [eq] (at 100) < [≡] (at 150) < [⊑] (at 200). *)
 Global Instance equiv_rewrite_relation `{Equiv A} :
   RewriteRelation (@equiv A _) | 150 := {}.
 
@@ -1359,7 +1359,10 @@ Notation "(.⊑ y )" := (λ x, sqsubseteq x y) (only parsing) : stdpp_scope.
 Infix "⊑@{ A }" := (@sqsubseteq A _) (at level 70, only parsing) : stdpp_scope.
 Notation "(⊑@{ A } )" := (@sqsubseteq A _) (only parsing) : stdpp_scope.
 
-Global Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑@{A}) := {}.
+(** [sqsubseteq] does not take precedence over the stdlib's instances (like [eq],
+[impl], [iff]) or std++'s [equiv].
+We have [eq] (at 100) < [≡] (at 150) < [⊑] (at 200). *)
+Global Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑@{A}) | 200 := {}.
 
 Global Hint Extern 0 (_ ⊑ _) => reflexivity : core.