From 78bfc78bfb7824272326eb451ac79a3f21ab17c9 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Thu, 23 Apr 2020 16:18:35 +0200
Subject: [PATCH] Removed unnecessary use of frame rule

---
 theories/logrel/types.v | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

diff --git a/theories/logrel/types.v b/theories/logrel/types.v
index 37ae721..9f12f3b 100644
--- a/theories/logrel/types.v
+++ b/theories/logrel/types.v
@@ -205,13 +205,7 @@ Section properties.
   Lemma ltyped_let Γ1 Γ2 Γ3 (x : binder) e1 e2 A1 A2 :
     (Γ1 ⊨ e1 : A1 ⫤ Γ2) -∗ (binder_insert x A1 Γ2 ⊨ e2 : A2 ⫤ Γ3) -∗
     Γ1 ⊨ (let: x:=e1 in e2) : A2 ⫤ ∅.
-  Proof.
-    iIntros "#He1 #He2".
-    iApply ltyped_app=> //.
-    iApply (ltyped_frame _ _ _ _ ∅); last by iApply (ltyped_lam).
-    - iApply env_split_id_r.
-    - iApply env_split_empty.
-  Qed.
+  Proof. iIntros "#He1 #He2". iApply ltyped_app=> //. iApply ltyped_lam. Qed.
 
   Lemma ltyped_rec Γ Γ' f x e A1 A2 :
     env_copy Γ Γ' -∗
-- 
GitLab