diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index dc70d5ace9d051e8504bb18c5c1cf78b64f2cf33..372f36c14647317a00bedc1dcf1efa33ddfc0170 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -95,4 +95,4 @@ Notation "<!!> A ; P" :=
   (lsty_send A P) (at level 20, A, P at level 200) : lsty_scope.
 Notation "<??> A ; P" :=
   (lsty_recv A P) (at level 20, A, P at level 200) : lsty_scope.
-Infix "<++++>" := lsty_app (at level 60) : lsty_scope.
+Infix "<++>" := lsty_app (at level 60) : lsty_scope.
diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index 443e38eb883f7fc4f64a2f2a2668bbc40e94399c..90738127fdde9b2f25f52d231e40e131b2cc804d 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -285,7 +285,7 @@ Section subtype.
 
   Lemma lsty_app_le P11 P12 P21 P22 :
     (P11 <p: P21) -∗ (P12 <p: P22) -∗
-    (P11 <++++> P12) <p: (P21 <++++> P22).
+    (P11 <++> P12) <p: (P21 <++> P22).
   Proof. iIntros "#H1 #H2 !>". by iApply iProto_le_app. Qed.
 
   Lemma lsty_dual_le P1 P2 : P2 <p: P1 -∗ lsty_dual P1 <p: lsty_dual P2.