diff --git a/theories/base.v b/theories/base.v
index 763e86c419fa5f7b2811e25e14d87e0fa268c073..61d2b69a2206695ecaad52f4dbd0d36938a65baf 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1138,6 +1138,8 @@ Notation "( x ⊑)" := (sqsubseteq x) (only parsing) : stdpp_scope.
 Notation "(⊑ y )" := (λ x, sqsubseteq x y) (only parsing) : stdpp_scope.
 Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑).
 
+Hint Extern 0 (_ ⊑ _) => reflexivity.
+
 Class Meet A := meet: A → A → A.
 Hint Mode Meet ! : typeclass_instances.
 Instance: Params (@meet) 2.