From d1f06c73b7cf4936d3ea4ba0ab33c679064a10f7 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Tue, 15 Sep 2020 13:57:14 +0200
Subject: [PATCH] Removed unused variable from app choice lemmas
---
theories/logrel/subtyping_rules.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index db0c667..3a3cc7d 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -448,10 +448,10 @@ Section subtyping_rules.
iSplit; iIntros "!> /="; destruct a;
iIntros (x); iExists x; iDestruct 1 as %[S ->]; iSplitR; eauto.
Qed.
- Lemma lty_le_app_select A Ss S2 :
+ Lemma lty_le_app_select Ss S2 :
⊢ lty_select Ss <++> S2 <:> lty_select ((.<++> S2) <$> Ss)%lty.
Proof. apply lty_le_app_choice. Qed.
- Lemma lty_le_app_branch A Ss S2 :
+ Lemma lty_le_app_branch Ss S2 :
⊢ lty_branch Ss <++> S2 <:> lty_branch ((.<++> S2) <$> Ss)%lty.
Proof. apply lty_le_app_choice. Qed.
--
GitLab