From d55bc65a4d2577f87bd42ab844c2cba6e430310f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 4 May 2020 09:07:07 +0200
Subject: [PATCH] Stronger variable rule.

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

diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index 3cdacfd..54e5fdd 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -16,11 +16,14 @@ Section properties.
 
   (** Variable properties *)
   Lemma ltyped_var Γ (x : string) A :
-    Γ !! x = Some A → ⊢ Γ ⊨ x : A ⫤ delete x Γ.
+    Γ !! x = Some A → ⊢ Γ ⊨ x : A ⫤ <[x:=copy- A]>%lty Γ.
   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.
+    iDestruct (env_ltyped_lookup with "HΓ") as (v Hx) "[HA HΓ]"; first done.
+    rewrite Hx. iApply wp_value.
+    iDestruct (coreP_intro with "HA") as "#HAc". iFrame "HA".
+    iEval (rewrite -insert_delete -(insert_id vs x v) //).
+    by iApply (env_ltyped_insert _ _ x).
   Qed.
 
   (** Subtyping *)
-- 
GitLab