From 800308d26df46a775a861b688b3dc7fc9d6fe584 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Thu, 23 Apr 2020 11:38:42 +0200
Subject: [PATCH] Updated Lam/Let

---
 theories/logrel/types.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/logrel/types.v b/theories/logrel/types.v
index 54aa0e4..bce95ea 100644
--- a/theories/logrel/types.v
+++ b/theories/logrel/types.v
@@ -192,7 +192,7 @@ Section properties.
 
   Lemma ltyped_lam Γ Γ1 Γ2 x e A1 A2 :
     (<[ x := A1 ]>Γ ⊨ e : A2 ⫤ Γ2) -∗
-    Γ ⊨ (λ: x, e) : A1 ⊸ A2 ⫤ Γ2.
+    Γ ⊨ (λ: x, e) : A1 ⊸ A2 ⫤ binder_delete x Γ2.
   Proof.
     iIntros "#He" (vs) "!> HΓ /=".
     wp_pures.
@@ -207,10 +207,10 @@ Section properties.
 
   Lemma ltyped_let Γ1 Γ2 Γ3 (x : binder) e1 e2 A1 A2 :
     (Γ1 ⊨ e1 : A1 ⫤ Γ2) -∗ (<[x:=A1]>Γ2 ⊨ e2 : A2 ⫤ Γ3) -∗
-    Γ1 ⊨ (let: x:=e1 in e2) : A2 ⫤ Γ3.
+    Γ1 ⊨ (let: x:=e1 in e2) : A2 ⫤ binder_delete x Γ3.
   Proof.
     iIntros "#He1 #He2".
-    iApply ltyped_app=> //.
+    iApply ltyped_app=> //.    
     iApply (ltyped_lam)=> //.
   Qed.
 
-- 
GitLab