diff --git a/theories/base.v b/theories/base.v
index 81f9078bf95e40c552b2bef27c67e974ea4cf775..2b00af030f368b8bc024e982db668fed82ae1be1 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -866,6 +866,10 @@ Notation "{[ x ; y ; .. ; z ]}" :=
   (union .. (union (singleton x) (singleton y)) .. (singleton z))
   (at level 1) : stdpp_scope.
 
+Notation "+{[ x ; y ; .. ; z ]}" :=
+  (disj_union .. (disj_union (singleton x) (singleton y)) .. (singleton z))
+  (at level 1) : stdpp_scope.
+
 Class SubsetEq A := subseteq: relation A.
 Global Hint Mode SubsetEq ! : typeclass_instances.
 Instance: Params (@subseteq) 2 := {}.