diff --git a/theories/base.v b/theories/base.v
index 571ac7d77bebdac7ccd68dc7bf05a4bcd44d5eea..b229cba6bd0884bd5cfd379df236cd6f8c22e453 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1204,6 +1204,10 @@ Infix "⊑" := sqsubseteq (at level 70) : stdpp_scope.
 Notation "(⊑)" := sqsubseteq (only parsing) : stdpp_scope.
 Notation "( x ⊑)" := (sqsubseteq x) (only parsing) : stdpp_scope.
 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.
+
 Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑).
 
 Hint Extern 0 (_ ⊑ _) => reflexivity.