From f765e44bb9fd2e3f3812e41d1c0b7f38ca83e76b Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Fri, 5 Jun 2020 10:47:45 +0200
Subject: [PATCH] Changed order of premises in frame rule

---
 theories/logrel/examples/mapper.v   | 22 +++++++++++-----------
 theories/logrel/term_typing_rules.v |  4 ++--
 2 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/theories/logrel/examples/mapper.v b/theories/logrel/examples/mapper.v
index e33c44d..65ae3aa 100644
--- a/theories/logrel/examples/mapper.v
+++ b/theories/logrel/examples/mapper.v
@@ -23,21 +23,21 @@ Section with_Σ.
     iApply ltyped_let.
     { iApply ltyped_recv. by rewrite insert_commute // lookup_insert. }
     rewrite (insert_commute _ "c" "f") // insert_insert.
-    iApply (ltyped_let _ (<["c":= lty_chan END]>_))=> /=; last first.
+    iApply ltyped_let=> /=; last first.
     { iApply ltyped_var. apply lookup_insert. }
-    rewrite (insert_commute _ "f" "c") // (insert_commute _ "v" "c") //.
     iApply ltyped_send. apply lookup_insert.
+    rewrite (insert_commute _ "f" "c") // (insert_commute _ "v" "c") //.
     iApply (ltyped_frame _ _ _ _ {["c":=_]}).
     { iApply env_split_right=> //. iApply env_split_id_r. }
-    { iApply env_split_right=> //. shelve. iApply env_split_id_r. }
-    iApply ltyped_app.
-    - iApply ltyped_var. apply lookup_insert.
-    - rewrite insert_commute //.
-      iApply (ltyped_frame _ _ _ _ {["f":=_]}).
-      { iApply env_split_right=> //. iApply env_split_id_r. }
-      { iApply env_split_right=> //. shelve. iApply env_split_id_r. }
-      iApply ltyped_var. apply lookup_insert.
-      Unshelve. eauto. eauto.
+    { iApply ltyped_app.
+      - iApply ltyped_var. apply lookup_insert.
+      - rewrite insert_commute //.
+        iApply (ltyped_frame _ _ _ _ {["f":=_]}).
+        { iApply env_split_right=> //. iApply env_split_id_r. }
+        { iApply ltyped_var. apply lookup_insert. }
+        { iApply env_split_right=> //; last by iApply env_split_id_r. eauto. }
+    }
+    { iApply env_split_right=> //; last by iApply env_split_id_r. eauto. }
   Qed.
 
 End with_Σ.
diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index 54f29b0..f8aef55 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -20,11 +20,11 @@ Section properties.
   (** Frame rule *)
   Lemma ltyped_frame Γ Γ' Γ1 Γ1' Γ2 e A :
     env_split Γ Γ1 Γ2 -∗
-    env_split Γ' Γ1' Γ2 -∗
     (Γ1 ⊨ e : A ⫤ Γ1') -∗
+    env_split Γ' Γ1' Γ2 -∗
     Γ ⊨ e : A ⫤ Γ'.
   Proof.
-    iIntros "#Hsplit #Hsplit' #Htyped !>" (vs) "Henv".
+    iIntros "#Hsplit #Htyped #Hsplit' !>" (vs) "Henv".
     iDestruct ("Hsplit" with "Henv") as "[Henv1 Henv2]".
     iApply (wp_wand with "(Htyped Henv1)").
     iIntros (v) "[$ Henv1']".
-- 
GitLab