diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index 14f4dfa1ef85b8f49bcc9b277565cc9cc9bd2f05..eecd13a61b4f7ec2770dce7a5a41175e4e704dda 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -50,6 +50,9 @@ Notation "<!! X .. Y > M" :=
   (<!!> ∃ X, .. (∃ Y, M) ..)%lty
     (at level 200, X closed binder, Y closed binder, M at level 200,
      format "<!!  X  ..  Y >  M") : lty_scope.
+Notation "<!!.. X .. Y > M" := (<!!> ∃.. X, .. (∃.. Y, M) ..)%lty
+  (at level 200, X closed binder, Y closed binder, M at level 200,
+   format "<!!..  X  ..  Y >  M") : lty_scope.
 
 Notation "<??> M" :=
   (lty_message Recv M) (at level 200, M at level 200) : lty_scope.
@@ -57,6 +60,9 @@ Notation "<?? X .. Y > M" :=
   (<??> ∃ X, .. (∃ Y, M) ..)%lty
     (at level 200, X closed binder, Y closed binder, M at level 200,
      format "<??  X  ..  Y >  M") : lty_scope.
+Notation "<??.. X .. Y > M" := (<??> ∃.. X, .. (∃.. Y, M) ..)%lty
+  (at level 200, X closed binder, Y closed binder, M at level 200,
+   format "<??..  X  ..  Y >  M") : lty_scope.
 Notation lty_select := (lty_choice Send).
 Notation lty_branch := (lty_choice Recv).
 Infix "<++>" := lty_app (at level 60) : lty_scope.