From 67599f5ade3c8eb01d6d077357d9afe2dbcb9eeb Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Fri, 17 Apr 2020 16:39:13 +0200
Subject: [PATCH] Fixed copy paste blunder

---
 theories/logrel/subtyping.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index 4901791..9aa0108 100644
--- a/theories/logrel/subtyping.v
+++ b/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 :
-- 
GitLab