From e0199d4bfb2e31294265d19abb60d98c3eec68ba Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Thu, 2 Jul 2020 09:09:26 +0200
Subject: [PATCH] Errata

---
 theories/logrel/subtyping_rules.v | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index eee85cf..d27f187 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -351,10 +351,9 @@ Section subtyping_rules.
   Lemma lty_le_swap_branch_select (Ss1 Ss2 : (gmap Z (gmap Z (lsty Σ)))) :
     (∀ i j Ss1' Ss2',
         Ss1 !! i = Some Ss1' → Ss2 !! j = Some Ss2' →
-        (is_Some (Ss1' !! j) ∧ is_Some (Ss2' !! i) ∧
-        Ss1' !! j = Ss2' !! i)) →
-    ⊢ lty_branch ((λ Ss, lty_select Ss) <$> Ss1) <:
-      lty_select ((λ Ss, lty_branch Ss) <$> Ss2).
+        is_Some (Ss1' !! j) ∧ is_Some (Ss2' !! i) ∧
+        Ss1' !! j = Ss2' !! i) →
+    ⊢ lty_branch (lty_select <$> Ss1) <: lty_select (lty_branch <$> Ss2).
   Proof.
     intros Hin.
     iIntros "!>" (v1 v2).
-- 
GitLab