From 03758fe253ccefb1baa8ac0c83fc15cbb3fc0abc Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Mon, 4 May 2020 13:40:18 +0200
Subject: [PATCH] Updated variable rule to be in line with paper version

---
 theories/logrel/term_typing_rules.v | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index 3cdacfd..6e5cc11 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -16,11 +16,13 @@ Section properties.
 
   (** Variable properties *)
   Lemma ltyped_var Γ (x : string) A :
-    Γ !! x = Some A → ⊢ Γ ⊨ x : A ⫤ delete x Γ.
+    ⊢ <[x := A]>Γ ⊨ x : A ⫤ delete x Γ.
   Proof.
-    iIntros (HΓx) "!>"; iIntros (vs) "HΓ /=".
-    iDestruct (env_ltyped_lookup with "HΓ") as (v ->) "[HA HΓ]"; first done.
-    iApply wp_value. eauto with iFrame.
+    iIntros "!>" (vs) "HΓ /=".
+    iDestruct (env_ltyped_lookup with "HΓ") as (v ->) "[HA HΓ]";
+      first by apply lookup_insert.
+    iApply wp_value. iFrame "HA".
+    by rewrite delete_insert_delete.
   Qed.
 
   (** Subtyping *)
-- 
GitLab