From deee9548e3cac3095f7723d1bd33dabf71d69c71 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Thu, 4 Jun 2020 13:11:27 +0200
Subject: [PATCH] Minor rule simplification

---
 theories/logrel/term_typing_judgment.v | 4 +---
 theories/logrel/term_typing_rules.v    | 3 +--
 2 files changed, 2 insertions(+), 5 deletions(-)

diff --git a/theories/logrel/term_typing_judgment.v b/theories/logrel/term_typing_judgment.v
index c164c03..4df8780 100644
--- a/theories/logrel/term_typing_judgment.v
+++ b/theories/logrel/term_typing_judgment.v
@@ -29,8 +29,6 @@ Lemma ltyped_safety `{heapPreG Σ} e σ es σ' e' :
 Proof.
   intros Hty. apply (heap_adequacy Σ NotStuck e σ (λ _, True))=> // ?.
   destruct (Hty _) as (A & Γ' & He). iIntros "_".
-  iDestruct (He) as "He".
-  iSpecialize ("He" $!∅).
-  iSpecialize ("He" with "[]"); first by rewrite /env_ltyped.
+  iDestruct (He $!∅ with "[]") as "He"; first by rewrite /env_ltyped.
   iEval (rewrite -(subst_map_empty e)). iApply (wp_wand with "He"); auto.
 Qed.
diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index d5c4b25..2637dbd 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -79,8 +79,7 @@ Section properties.
     Γ ⊨ (λ: x, e) : A1 ⊸ A2 ⫤ ∅.
   Proof.
     iIntros "#He" (vs) "!> HΓ /=".
-    wp_pures.
-    iSplitL; last by iApply env_ltyped_empty.
+    wp_pures. iSplitL; last by iApply env_ltyped_empty.
     iIntros (v) "HA1". wp_pures.
     iDestruct ("He" $!((binder_insert x v vs)) with "[HA1 HΓ]") as "He'".
     { iApply (env_ltyped_insert with "[HA1 //] HΓ"). }
-- 
GitLab