Changed order of premises in frame rule

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_Σ.

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']".