diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 5fcb5966e3ae5d3b2643b57938b5784e29081820..bc2c943b1788532e7f8ad626f07c442ac4929f19 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -45,7 +45,7 @@ Module Type lifetime_sig.
 
   (** * Notation *)
   Notation "q .[ κ ]" := (lft_tok q κ)
-      (format "q .[ κ ]", at level 0) : bi_scope.
+      (format "q .[ κ ]", at level 2, left associativity) : bi_scope.
   Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): bi_scope.
 
   Notation "&{ κ }" := (bor κ) (format "&{ κ }") : bi_scope.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index f1e0adff9adf3d72a942556c034e45f06b08de58..b4556a06603292f67377da5934c14ca9c87f79c7 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -207,7 +207,7 @@ Instance raw_bor_params : Params (@raw_bor) 4 := {}.
 Instance bor_params : Params (@bor) 4 := {}.
 
 Notation "q .[ κ ]" := (lft_tok q κ)
-    (format "q .[ κ ]", at level 0) : bi_scope.
+    (format "q .[ κ ]", at level 2, left associativity) : bi_scope.
 Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): bi_scope.
 
 Notation "&{ κ }" := (bor κ) (format "&{ κ }") : bi_scope.