diff --git a/theories/base.v b/theories/base.v
index df6f279610e60dcf347722004278fa53a47dd0eb..b55691235839c7fa8e1be4473c408a6fd76bfb10 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -256,7 +256,10 @@ 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]).
+  [eq] (at 100) < [≡] (at 150) < [⊑] (at 200).  
+
+*)
 Global Instance equiv_rewrite_relation `{Equiv A} :
   RewriteRelation (@equiv A _) | 150 := {}.
 
@@ -1359,8 +1362,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.
 
-(** [sqsubseteq] does not take precedence over the stdlib's instances or [equiv]. *)
-Global Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑@{A}) | 160 := {}.
+(** [sqsubseteq] does not take precedence over the stdlib's instances or [equiv].
+  [eq] (at 100) < [≡] (at 150) < [⊑] (at 200).  
+*)
+Global Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑@{A}) | 200 := {}.
 
 Global Hint Extern 0 (_ ⊑ _) => reflexivity : core.