Set the priority of the rewrite relation for sqsubseteq to not take precedence over...

Set the priority of the rewrite relation for sqsubseteq to not take precedence over the eq instance from Coq or equiv.

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,7 +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.
 
-Global Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑@{A}) := {}.
+(** [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.