Fixed copy paste blunder

theories/logrel/subtyping.v

@@ -293,7 +293,7 @@ Section subtype.
   Proof. iIntros "#H1 #H2 !>". by iApply iProto_le_app. Qed.
 
   Lemma lsty_le_app_assoc_l S1 S2 S3 :
-    ⊢ ((S1 <++> S2) <++> S3) <s: (S1 <++> (S2 <++> S3)).
+    ⊢ (S1 <++> (S2 <++> S3)) <s: ((S1 <++> S2) <++> S3).
   Proof. rewrite lsty_app_assoc. iApply lsty_le_refl. Qed.
 
   Lemma lsty_le_app_assoc_r S1 S2 S3 :

[Robbert Krebbers]

The outer parens are redundant.