From 3abc933bf0f24cc63faf89241631a1b6cb1deb2b Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 24 Nov 2016 14:34:31 +0100
Subject: [PATCH] Use the new validity notations. Curry more things.

---
 iris                   |  2 +-
 theories/derived.v     | 18 ++++++------
 theories/frac_borrow.v | 16 +++++------
 theories/heap.v        |  6 ++--
 theories/lifetime.v    | 64 +++++++++++++++++++++---------------------
 theories/lifting.v     | 20 ++++++-------
 theories/perm.v        |  9 +++---
 theories/perm_incl.v   |  6 ++--
 theories/shr_borrow.v  |  6 ++--
 theories/tl_borrow.v   |  4 +--
 theories/type.v        | 18 ++++++------
 theories/type_incl.v   | 15 +++++-----
 theories/typing.v      | 49 ++++++++++++++++----------------
 13 files changed, 116 insertions(+), 117 deletions(-)

diff --git a/iris b/iris
index 36c5a842..243fdd13 160000
--- a/iris
+++ b/iris
@@ -1 +1 @@
-Subproject commit 36c5a84241841fadffaee32c710680b3c0d88eb0
+Subproject commit 243fdd139ccdf1370e5b186650e4323d5e73e54b
diff --git a/theories/derived.v b/theories/derived.v
index a7c7ad94..1a2180de 100644
--- a/theories/derived.v
+++ b/theories/derived.v
@@ -25,35 +25,35 @@ Lemma wp_lam E xl e e' el Φ :
   Forall (λ ei, is_Some (to_val ei)) el →
   Closed (xl +b+ []) e →
   subst_l xl el e = Some e' →
-  ▷ WP e' @ E {{ Φ }} ⊢ WP App (Lam xl e) el @ E {{ Φ }}.
+  ▷ WP e' @ E {{ Φ }} -∗ WP App (Lam xl e) el @ E {{ Φ }}.
 Proof. iIntros (???) "?". by iApply (wp_rec _ _ BAnon). Qed.
 
 Lemma wp_let E x e1 e2 v Φ :
   to_val e1 = Some v →
   Closed (x :b: []) e2 →
-  ▷ WP subst' x e1 e2 @ E {{ Φ }} ⊢ WP Let x e1 e2 @ E {{ Φ }}.
+  ▷ WP subst' x e1 e2 @ E {{ Φ }} -∗ WP Let x e1 e2 @ E {{ Φ }}.
 Proof. eauto using wp_lam. Qed.
 
 Lemma wp_seq E e1 e2 v Φ :
   to_val e1 = Some v →
   Closed [] e2 →
-  ▷ WP e2 @ E {{ Φ }} ⊢ WP Seq e1 e2 @ E {{ Φ }}.
+  ▷ WP e2 @ E {{ Φ }} -∗ WP Seq e1 e2 @ E {{ Φ }}.
 Proof. iIntros (??) "?". by iApply (wp_let _ BAnon). Qed.
 
-Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) ⊢ WP Skip @ E {{ Φ }}.
+Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) -∗ WP Skip @ E {{ Φ }}.
 Proof. iIntros. iApply wp_seq. done. iNext. by iApply wp_value. Qed.
 
 Lemma wp_le E (n1 n2 : Z) P Φ :
-  (n1 ≤ n2 → P ⊢ ▷ |={E}=> Φ (LitV true)) →
-  (n2 < n1 → P ⊢ ▷ |={E}=> Φ (LitV false)) →
-  P ⊢ WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
+  (n1 ≤ n2 → P -∗ ▷ |={E}=> Φ (LitV true)) →
+  (n2 < n1 → P -∗ ▷ |={E}=> Φ (LitV false)) →
+  P -∗ WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
 Proof.
   intros. rewrite -wp_bin_op //; [].
   destruct (bool_decide_reflect (n1 ≤ n2)); by eauto with omega.
 Qed.
 
 Lemma wp_if E (b : bool) e1 e2 Φ :
-  (if b then ▷ WP e1 @ E {{ Φ }} else ▷ WP e2 @ E {{ Φ }})%I
-  ⊢ WP If (Lit b) e1 e2 @ E {{ Φ }}.
+  (if b then ▷ WP e1 @ E {{ Φ }} else ▷ WP e2 @ E {{ Φ }})%I -∗
+  WP If (Lit b) e1 e2 @ E {{ Φ }}.
 Proof. iIntros "?". by destruct b; iApply wp_case. Qed.
 End derived.
diff --git a/theories/frac_borrow.v b/theories/frac_borrow.v
index 9f1535a5..64f595dd 100644
--- a/theories/frac_borrow.v
+++ b/theories/frac_borrow.v
@@ -22,7 +22,7 @@ Section frac_borrow.
   Global Instance frac_borrow_persistent : PersistentP (&frac{κ}Φ) := _.
 
   Lemma borrow_fracture φ E κ :
-    ↑lftN ⊆ E → lft_ctx ⊢ &{κ}(φ 1%Qp) ={E}=∗ &frac{κ}φ.
+    ↑lftN ⊆ E → lft_ctx -∗ &{κ}(φ 1%Qp) ={E}=∗ &frac{κ}φ.
   Proof.
     iIntros (?) "#LFT Hφ". iMod (own_alloc 1%Qp) as (γ) "?". done.
     iMod (borrow_acc_atomic_strong with "LFT Hφ") as "[[Hφ Hclose]|[H† Hclose]]". done.
@@ -40,7 +40,7 @@ Section frac_borrow.
 
   Lemma frac_borrow_atomic_acc E κ φ :
     ↑lftN ⊆ E →
-    lft_ctx ⊢ &frac{κ}φ ={E,E∖↑lftN}=∗ (∃ q, ▷ φ q ∗ (▷ φ q ={E∖↑lftN,E}=∗ True))
+    lft_ctx -∗ &frac{κ}φ ={E,E∖↑lftN}=∗ (∃ q, ▷ φ q ∗ (▷ φ q ={E∖↑lftN,E}=∗ True))
                                       ∨ [†κ] ∗ |={E∖↑lftN,E}=> True.
   Proof.
     iIntros (?) "#LFT #Hφ". iDestruct "Hφ" as (γ κ') "[Hκκ' Hshr]".
@@ -53,7 +53,7 @@ Section frac_borrow.
 
   Lemma frac_borrow_acc_strong E q κ Φ:
     ↑lftN ⊆ E →
-    lft_ctx ⊢ □ (∀ q1 q2, Φ (q1+q2)%Qp ↔ Φ q1 ∗ Φ q2) -∗
+    lft_ctx -∗ □ (∀ q1 q2, Φ (q1+q2)%Qp ↔ Φ q1 ∗ Φ q2) -∗
     &frac{κ}Φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ Φ q' ∗ (▷ Φ q' ={E}=∗ q.[κ]).
   Proof.
     iIntros (?) "#LFT #HΦ Hfrac Hκ". unfold frac_borrow.
@@ -99,20 +99,20 @@ Section frac_borrow.
 
   Lemma frac_borrow_acc E q κ `{Fractional _ Φ} :
     ↑lftN ⊆ E →
-    lft_ctx ⊢ &frac{κ}Φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ Φ q' ∗ (▷ Φ q' ={E}=∗ q.[κ]).
+    lft_ctx -∗ &frac{κ}Φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ Φ q' ∗ (▷ Φ q' ={E}=∗ q.[κ]).
   Proof.
     iIntros (?) "LFT". iApply (frac_borrow_acc_strong with "LFT"). done.
     iIntros "!#*". rewrite fractional. iSplit; auto.
   Qed.
 
-  Lemma frac_borrow_shorten κ κ' Φ: κ ⊑ κ' ⊢ &frac{κ'}Φ -∗ &frac{κ}Φ.
+  Lemma frac_borrow_shorten κ κ' Φ: κ ⊑ κ' -∗ &frac{κ'}Φ -∗ &frac{κ}Φ.
   Proof.
-    iIntros "Hκκ' H". iDestruct "H" as (γ κ0) "[H⊑?]". iExists γ, κ0. iFrame.
-    iApply lft_incl_trans. iFrame.
+    iIntros "Hκκ' H". iDestruct "H" as (γ κ0) "[#H⊑ ?]". iExists γ, κ0. iFrame.
+    iApply (lft_incl_trans with "Hκκ' []"). auto.
   Qed.
 
   Lemma frac_borrow_incl κ κ' q:
-    lft_ctx ⊢ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
+    lft_ctx -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
   Proof.
     iIntros "#LFT#Hbor!#". iSplitR.
     - iIntros (q') "Hκ'".
diff --git a/theories/heap.v b/theories/heap.v
index 58d0bf7c..dbe54f5e 100644
--- a/theories/heap.v
+++ b/theories/heap.v
@@ -187,7 +187,7 @@ Section heap.
   Qed.
 
   Lemma heap_mapsto_vec_prop_op l q1 q2 n (Φ : list val → iProp Σ) :
-    (∀ vl, Φ vl ⊢ ⌜length vl = n⌝) →
+    (∀ vl, Φ vl -∗ ⌜length vl = n⌝) →
     l ↦∗{q1}: Φ ∗ l ↦∗{q2}: (λ vl, ⌜length vl = n⌝) ⊣⊢ l ↦∗{q1+q2}: Φ.
   Proof.
     intros Hlen. iSplit.
@@ -396,7 +396,7 @@ Section heap.
   Qed.
 
   Lemma heap_mapsto_lookup l ls q v σ:
-    own heap_name (● to_heap σ) ⊢
+    own heap_name (● to_heap σ) -∗
     own heap_name (◯ {[ l := (q, to_lock_stateR ls, DecAgree v) ]}) -∗
     ⌜∃ n' : nat,
         σ !! l = Some (match ls with RSt n => RSt (n+n') | WSt => WSt end, v)⌝.
@@ -414,7 +414,7 @@ Section heap.
   Qed.
 
   Lemma heap_mapsto_lookup_1 l ls v σ:
-    own heap_name (● to_heap σ) ⊢
+    own heap_name (● to_heap σ) -∗
     own heap_name (◯ {[ l := (1%Qp, to_lock_stateR ls, DecAgree v) ]}) -∗
     ⌜σ !! l = Some (ls, v)⌝.
   Proof.
diff --git a/theories/lifetime.v b/theories/lifetime.v
index a63ba53d..3f4cbe57 100644
--- a/theories/lifetime.v
+++ b/theories/lifetime.v
@@ -71,7 +71,7 @@ Hint Unfold lifetime : typeclass_instances.
 Section lft.
   Context `{invG Σ, lifetimeG Σ}.
 
-  Axiom lft_ctx_alloc : True ={∅}=∗ lft_ctx.
+  Axiom lft_ctx_alloc : (|={∅}=> lft_ctx)%I.
 
   (*** PersitentP, TimelessP, Proper and Fractional instances  *)
 
@@ -140,41 +140,41 @@ Section lft.
 
   Axiom idx_borrow_acc :
     ∀ `(↑lftN ⊆ E) q κ i P,
-      lft_ctx ⊢ idx_borrow κ i P -∗ idx_borrow_own 1 i
+      lft_ctx -∗ idx_borrow κ i P -∗ idx_borrow_own 1 i
               -∗ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ idx_borrow_own 1 i ∗ q.[κ]).
   Axiom idx_borrow_atomic_acc :
     ∀ `(↑lftN ⊆ E) q κ i P,
-      lft_ctx ⊢ idx_borrow κ i P -∗ idx_borrow_own q i
+      lft_ctx -∗ idx_borrow κ i P -∗ idx_borrow_own q i
          ={E,E∖↑lftN}=∗
             ▷ P ∗ (▷ P ={E∖↑lftN,E}=∗ idx_borrow_own q i) ∨
             [†κ] ∗ (|={E∖↑lftN,E}=> idx_borrow_own q i).
 
   (** Basic borrows  *)
   Axiom borrow_create :
-    ∀ `(↑lftN ⊆ E) κ P, lft_ctx ⊢ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
-  Axiom borrow_fake : ∀ `(↑lftN ⊆ E) κ P, lft_ctx ⊢ [†κ] ={E}=∗ &{κ}P.
+    ∀ `(↑lftN ⊆ E) κ P, lft_ctx -∗ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
+  Axiom borrow_fake : ∀ `(↑lftN ⊆ E) κ P, lft_ctx -∗ [†κ] ={E}=∗ &{κ}P.
   Axiom borrow_split :
-    ∀ `(↑lftN ⊆ E) κ P Q, lft_ctx ⊢ &{κ}(P ∗ Q) ={E}=∗ &{κ}P ∗ &{κ}Q.
+    ∀ `(↑lftN ⊆ E) κ P Q, lft_ctx -∗ &{κ}(P ∗ Q) ={E}=∗ &{κ}P ∗ &{κ}Q.
   Axiom borrow_combine :
-    ∀ `(↑lftN ⊆ E) κ P Q, lft_ctx ⊢ &{κ}P -∗ &{κ}Q ={E}=∗ &{κ}(P ∗ Q).
+    ∀ `(↑lftN ⊆ E) κ P Q, lft_ctx -∗ &{κ}P -∗ &{κ}Q ={E}=∗ &{κ}(P ∗ Q).
   Axiom borrow_acc_strong :
     ∀ `(↑lftN ⊆ E) q κ P,
-      lft_ctx ⊢ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗
+      lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗
       ∀ Q, ▷ Q ∗ ▷([†κ] -∗ ▷Q ={⊤ ∖ ↑lftN}=∗ ▷ P) ={E}=∗ &{κ}Q ∗ q.[κ].
   Axiom borrow_acc_atomic_strong :
     ∀ `(↑lftN ⊆ E) κ P,
-      lft_ctx ⊢ &{κ}P ={E,E∖↑lftN}=∗
+      lft_ctx -∗ &{κ}P ={E,E∖↑lftN}=∗
         (▷ P ∗ ∀ Q, ▷ Q ∗ ▷([†κ] -∗ ▷Q ={⊤ ∖ ↑lftN}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ}Q) ∨
         [†κ] ∗ |={E∖↑lftN,E}=> True.
   Axiom borrow_reborrow' :
     ∀ `(↑lftN ⊆ E) κ κ' P, κ ≼ κ' →
-      lft_ctx ⊢ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
+      lft_ctx -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
   Axiom borrow_unnest :
-    ∀ `(↑lftN ⊆ E) κ κ' P, lft_ctx ⊢ &{κ'}&{κ}P ={E, E∖↑lftN}▷=∗ &{κ ⋅ κ'}P.
+    ∀ `(↑lftN ⊆ E) κ κ' P, lft_ctx -∗ &{κ'}&{κ}P ={E, E∖↑lftN}▷=∗ &{κ ⋅ κ'}P.
 
   (*** Derived lemmas  *)
 
-  Lemma lft_own_dead q κ : q.[κ] ⊢ [† κ] -∗ False.
+  Lemma lft_own_dead q κ : q.[κ] -∗ [† κ] -∗ False.
   Proof.
     rewrite /lft_own /lft_dead.
     iIntros "Hl Hr". iDestruct "Hr" as (Λ) "[HΛ Hr]".
@@ -184,13 +184,13 @@ Section lft.
     by rewrite lookup_op lookup_singleton lookup_fmap lookup_omap HΛ.
   Qed.
 
-  Lemma lft_own_static q : True ==∗ q.[static].
+  Lemma lft_own_static q : (|==> q.[static])%I.
   Proof.
     rewrite /lft_own /static omap_empty fmap_empty.
     apply (own_empty lft_tokUR lft_toks_name).
   Qed.
 
-  Lemma lft_not_dead_static : [† static] ⊢ False.
+  Lemma lft_not_dead_static : [† static] -∗ False.
   Proof.
     rewrite /lft_dead /static. setoid_rewrite lookup_empty.
     iIntros "HΛ". iDestruct "HΛ" as (Λ) "[% _]". naive_solver.
@@ -206,7 +206,7 @@ Section lft.
 
   Lemma borrow_acc E q κ P :
     ↑lftN ⊆ E →
-    lft_ctx ⊢ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ &{κ}P ∗ q.[κ]).
+    lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ &{κ}P ∗ q.[κ]).
   Proof.
     iIntros (?) "#LFT HP Htok".
     iMod (borrow_acc_strong with "LFT HP Htok") as "[HP Hclose]". done.
@@ -215,7 +215,7 @@ Section lft.
 
   Lemma borrow_exists {A} E κ (Φ : A → iProp Σ) {_:Inhabited A}:
     ↑lftN ⊆ E →
-    lft_ctx ⊢ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
+    lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
   Proof.
     iIntros (?) "#LFT Hb".
     iMod (borrow_acc_atomic_strong with "LFT Hb") as "[[HΦ Hclose]|[H† Hclose]]". done.
@@ -224,7 +224,7 @@ Section lft.
   Qed.
 
   Lemma borrow_or E κ P Q:
-    ↑lftN ⊆ E → lft_ctx ⊢ &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q).
+    ↑lftN ⊆ E → lft_ctx -∗ &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q).
   Proof.
     iIntros (?) "#LFT H". rewrite uPred.or_alt.
     iMod (borrow_exists with "LFT H") as ([]) "H"; auto.
@@ -232,7 +232,7 @@ Section lft.
 
   Lemma borrow_persistent E `{PersistentP _ P} κ q:
     ↑lftN ⊆ E →
-    lft_ctx ⊢ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
+    lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
   Proof.
     iIntros (?) "#LFT Hb Htok".
     iMod (borrow_acc with "LFT Hb Htok") as "[#HP Hob]". done.
@@ -249,7 +249,7 @@ Definition lft_incl `{invG Σ, lifetimeG Σ} κ κ' : iProp Σ :=
   (□((∀ q, q.[κ] ={↑lftN}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={↑lftN}=∗ q.[κ])) ∗
      ([†κ'] ={↑lftN}=∗ [†κ])))%I.
 
-Infix "⊑" := lft_incl (at level 60) : C_scope.
+Infix "⊑" := lft_incl (at level 60) : uPred_scope.
 
 Section incl.
   Context `{invG Σ, lifetimeG Σ}.
@@ -258,31 +258,31 @@ Section incl.
 
   Lemma lft_incl_acc E κ κ' q:
     ↑lftN ⊆ E →
-    κ ⊑ κ' ⊢ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
+    κ ⊑ κ' -∗ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
   Proof.
     iIntros (?) "#[H _] Hq". iApply fupd_mask_mono. eassumption.
     iMod ("H" with "*Hq") as (q') "[Hq' Hclose]". iExists q'.
     iIntros "{$Hq'}!>Hq". iApply fupd_mask_mono. eassumption. by iApply "Hclose".
   Qed.
 
-  Lemma lft_incl_dead E κ κ': ↑lftN ⊆ E → κ ⊑ κ' ⊢ [†κ'] ={E}=∗ [†κ].
+  Lemma lft_incl_dead E κ κ': ↑lftN ⊆ E → κ ⊑ κ' -∗ [†κ'] ={E}=∗ [†κ].
   Proof.
     iIntros (?) "#[_ H] Hq". iApply fupd_mask_mono. eassumption. by iApply "H".
   Qed.
 
-  Lemma lft_le_incl κ κ': κ' ≼ κ → True ⊢ κ ⊑ κ'.
+  Lemma lft_le_incl κ κ': κ' ≼ κ → (κ ⊑ κ')%I.
   Proof.
     iIntros ([κ0 ->%leibniz_equiv]) "!#". iSplitR.
     - iIntros (q) "[Hκ' Hκ0]". iExists q. iIntros "!>{$Hκ'}Hκ'!>". by iSplitR "Hκ0".
     - iIntros "?!>". iApply lft_dead_or. auto.
   Qed.
 
-  Lemma lft_incl_refl κ : True ⊢ κ ⊑ κ.
+  Lemma lft_incl_refl κ : (κ ⊑ κ)%I.
   Proof. by apply lft_le_incl. Qed.
 
-  Lemma lft_incl_trans κ κ' κ'': κ ⊑ κ' ∗ κ' ⊑ κ'' ⊢ κ ⊑ κ''.
+  Lemma lft_incl_trans κ κ' κ'': κ ⊑ κ' -∗ κ' ⊑ κ'' -∗ κ ⊑ κ''.
   Proof.
-    unfold lft_incl. iIntros "[#[H1 H1†] #[H2 H2†]]!#". iSplitR.
+    unfold lft_incl. iIntros "#[H1 H1†] #[H2 H2†]!#". iSplitR.
     - iIntros (q) "Hκ".
       iMod ("H1" with "*Hκ") as (q') "[Hκ' Hclose]".
       iMod ("H2" with "*Hκ'") as (q'') "[Hκ'' Hclose']".
@@ -292,17 +292,17 @@ Section incl.
   Qed.
 
   Axiom idx_borrow_shorten :
-    ∀ κ κ' i P, κ ⊑ κ' ⊢ idx_borrow κ' i P -∗ idx_borrow κ i P.
+    ∀ κ κ' i P, κ ⊑ κ' -∗ idx_borrow κ' i P -∗ idx_borrow κ i P.
 
-  Lemma borrow_shorten κ κ' P: κ ⊑ κ' ⊢ &{κ'}P -∗ &{κ}P.
+  Lemma borrow_shorten κ κ' P: κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
   Proof.
     iIntros "H⊑ H". unfold borrow. iDestruct "H" as (i) "[??]".
     iExists i. iFrame. by iApply (idx_borrow_shorten with "H⊑").
   Qed.
 
-  Lemma lft_incl_lb κ κ' κ'' : κ ⊑ κ' ∗ κ ⊑ κ'' ⊢ κ ⊑ κ' ⋅ κ''.
+  Lemma lft_incl_lb κ κ' κ'' : κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ⋅ κ''.
   Proof.
-    iIntros "[#[H1 H1†] #[H2 H2†]]!#". iSplitR.
+    iIntros "#[H1 H1†] #[H2 H2†]!#". iSplitR.
     - iIntros (q) "[Hκ'1 Hκ'2]".
       iMod ("H1" with "*Hκ'1") as (q') "[Hκ' Hclose']".
       iMod ("H2" with "*Hκ'2") as (q'') "[Hκ'' Hclose'']".
@@ -314,7 +314,7 @@ Section incl.
     - rewrite -lft_dead_or. iIntros "[H†|H†]". by iApply "H1†". by iApply "H2†".
   Qed.
 
-  Lemma lft_incl_static κ : True ⊢ κ ⊑ static.
+  Lemma lft_incl_static κ : (κ ⊑ static)%I.
   Proof.
     iIntros "!#". iSplitR.
     - iIntros (q) "?". iExists 1%Qp. iSplitR. by iApply lft_own_static. auto.
@@ -322,12 +322,12 @@ Section incl.
   Qed.
 
   Lemma reborrow E P κ κ':
-    ↑lftN ⊆ E → lft_ctx ⊢ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗  &{κ}P).
+    ↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗  &{κ}P).
   Proof.
     iIntros (?) "#LFT #H⊑ HP".
     iMod (borrow_reborrow' with "LFT HP") as "[Hκ' H∋]". done. by exists κ'.
     iDestruct (borrow_shorten with "[H⊑] Hκ'") as "$".
-    { iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl. }
+    { iApply (lft_incl_lb with "[] []"). done. iApply lft_incl_refl. }
     iIntros "!>Hκ'". iApply ("H∋" with "[Hκ']"). iApply lft_dead_or. auto.
   Qed.
 
diff --git a/theories/lifting.v b/theories/lifting.v
index e3f6b3fa..4fead4c2 100644
--- a/theories/lifting.v
+++ b/theories/lifting.v
@@ -13,11 +13,11 @@ Implicit Types ef : option expr.
 
 (** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
 Lemma wp_bind {E e} K Φ :
-  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
+  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} -∗ WP fill K e @ E {{ Φ }}.
 Proof. exact: wp_ectx_bind. Qed.
 
 Lemma wp_bindi {E e} Ki Φ :
-  WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} ⊢
+  WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} -∗
      WP fill_item Ki e @ E {{ Φ }}.
 Proof. exact: weakestpre.wp_bind. Qed.
 
@@ -69,8 +69,8 @@ Lemma wp_read_na1_pst E l Φ :
   (|={E,∅}=> ∃ σ n v, ⌜σ !! l = Some(RSt $ n, v)⌝ ∧
      ▷ ownP σ ∗
      ▷ (ownP (<[l:=(RSt $ S n, v)]>σ) ={∅,E}=∗
-          WP Read Na2Ord (Lit $ LitLoc l) @ E {{ Φ }}))
-  ⊢ WP Read Na1Ord (Lit $ LitLoc l) @ E {{ Φ }}.
+          WP Read Na2Ord (Lit $ LitLoc l) @ E {{ Φ }})) -∗
+  WP Read Na1Ord (Lit $ LitLoc l) @ E {{ Φ }}.
 Proof.
   iIntros "HΦP". iApply (wp_lift_head_step E); auto.
   iMod "HΦP" as (σ n v) "(%&HΦ&HP)". iModIntro. iExists σ. iSplit. done. iFrame.
@@ -100,8 +100,8 @@ Lemma wp_write_na1_pst E l v Φ :
   (|={E,∅}=> ∃ σ v', ⌜σ !! l = Some(RSt 0, v')⌝ ∧
      ▷ ownP σ ∗
      ▷ (ownP (<[l:=(WSt, v')]>σ) ={∅,E}=∗
-       WP Write Na2Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }}))
-  ⊢ WP Write Na1Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }}.
+       WP Write Na2Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }})) -∗
+  WP Write Na1Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }}.
 Proof.
   iIntros "HΦP". iApply (wp_lift_head_step E); auto.
   iMod "HΦP" as (σ v') "(%&HΦ&HP)". iModIntro. iExists σ. iSplit. done. iFrame.
@@ -147,8 +147,8 @@ Lemma wp_rec E e f xl erec erec' el Φ :
   Forall (λ ei, is_Some (to_val ei)) el →
   Closed (f :b: xl +b+ []) erec →
   subst_l xl el erec = Some erec' →
-  ▷ WP subst' f e erec' @ E {{ Φ }}
-  ⊢ WP App e el @ E {{ Φ }}.
+  ▷ WP subst' f e erec' @ E {{ Φ }} -∗
+  WP App e el @ E {{ Φ }}.
 Proof.
   iIntros (-> ???) "?". iApply wp_lift_pure_det_head_step; subst; eauto.
   by intros; inv_head_step; eauto. iNext. rewrite big_sepL_nil. by iFrame.
@@ -156,7 +156,7 @@ Qed.
 
 Lemma wp_bin_op E op l1 l2 l' Φ :
   bin_op_eval op l1 l2 = Some l' →
-  ▷ (|={E}=> Φ (LitV l')) ⊢ WP BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
+  ▷ (|={E}=> Φ (LitV l')) -∗ WP BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_pure_det_head_step; eauto.
   by intros; inv_head_step; eauto.
@@ -166,7 +166,7 @@ Qed.
 Lemma wp_case E i e el Φ :
   0 ≤ i →
   nth_error el (Z.to_nat i) = Some e →
-  ▷ WP e @ E {{ Φ }} ⊢ WP Case (Lit $ LitInt i) el @ E {{ Φ }}.
+  ▷ WP e @ E {{ Φ }} -∗ WP Case (Lit $ LitInt i) el @ E {{ Φ }}.
 Proof.
   iIntros (??) "?". iApply wp_lift_pure_det_head_step; eauto.
   by intros; inv_head_step; eauto. iNext. rewrite big_sepL_nil. by iFrame.
diff --git a/theories/perm.v b/theories/perm.v
index 6638a701..ae364946 100644
--- a/theories/perm.v
+++ b/theories/perm.v
@@ -105,12 +105,13 @@ Section has_type.
   Qed.
 
   Lemma has_type_wp E (ν : expr) ty tid (Φ : val -> iProp _) :
-    (ν ◁ ty)%P tid ∗ (∀ (v : val), ⌜eval_expr ν = Some v⌝ ∗ (v ◁ ty)%P tid ={E}=∗ Φ v)
-    ⊢ WP ν @ E {{ Φ }}.
+    (ν ◁ ty)%P tid -∗
+    (∀ (v : val), ⌜eval_expr ν = Some v⌝ -∗ (v ◁ ty)%P tid ={E}=∗ Φ v) -∗
+    WP ν @ E {{ Φ }}.
   Proof.
-    iIntros "[H◁ HΦ]". setoid_rewrite has_type_value. unfold has_type.
+    iIntros "H◁ HΦ". setoid_rewrite has_type_value. unfold has_type.
     destruct (eval_expr ν) eqn:EQν; last by iDestruct "H◁" as "[]". simpl.
-    iMod ("HΦ" $! v with "[$H◁]") as "HΦ". done.
+    iMod ("HΦ" $! v with "[] H◁") as "HΦ". done.
     iInduction ν as [| | |[] e ? [|[]| | | | | | | | | |] _| | | | | | | |] "IH"
       forall (Φ v EQν); try done.
     - inversion EQν. subst. wp_value. auto.
diff --git a/theories/perm_incl.v b/theories/perm_incl.v
index 944f9b06..ff589d0e 100644
--- a/theories/perm_incl.v
+++ b/theories/perm_incl.v
@@ -10,13 +10,13 @@ Section defs.
 
   (* Definitions *)
   Definition perm_incl (ρ1 ρ2 : perm) :=
-    ∀ tid, lft_ctx ⊢ ρ1 tid ={⊤}=∗ ρ2 tid.
+    ∀ tid, lft_ctx -∗ ρ1 tid ={⊤}=∗ ρ2 tid.
 
   Global Instance perm_equiv : Equiv perm :=
     λ ρ1 ρ2, perm_incl ρ1 ρ2 ∧ perm_incl ρ2 ρ1.
 
   Definition borrowing κ (ρ ρ1 ρ2 : perm) :=
-    ∀ tid, lft_ctx ⊢ ρ tid -∗ ρ1 tid ={⊤}=∗ ρ2 tid ∗ (κ ∋ ρ1)%P tid.
+    ∀ tid, lft_ctx -∗ ρ tid -∗ ρ1 tid ={⊤}=∗ ρ2 tid ∗ (κ ∋ ρ1)%P tid.
 
 End defs.
 
@@ -99,7 +99,7 @@ Section props.
   Proof. iIntros (tid) "_ _!>". iApply lft_incl_refl. Qed.
 
   Lemma perm_lftincl_trans κ1 κ2 κ3 : κ1 ⊑ κ2 ∗ κ2 ⊑ κ3 ⇒ κ1 ⊑ κ3.
-  Proof. iIntros (tid) "_ [#?#?]!>". iApply lft_incl_trans. auto. Qed.
+  Proof. iIntros (tid) "_ [#?#?]!>". iApply (lft_incl_trans with "[] []"); auto. Qed.
 
   Lemma perm_incl_share q ν κ ty :
     ν ◁ &uniq{κ} ty ∗ q.[κ] ⇒ ν ◁ &shr{κ} ty ∗ q.[κ].
diff --git a/theories/shr_borrow.v b/theories/shr_borrow.v
index a4eed050..5987de8d 100644
--- a/theories/shr_borrow.v
+++ b/theories/shr_borrow.v
@@ -24,7 +24,7 @@ Section shared_borrows.
 
   Lemma shr_borrow_acc E κ :
     ↑lftN ⊆ E →
-    lft_ctx ⊢ &shr{κ}P ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ True) ∨
+    lft_ctx -∗ &shr{κ}P ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ True) ∨
                [†κ] ∗ |={E∖↑lftN,E}=> True.
   Proof.
     iIntros (?) "#LFT #HP". iDestruct "HP" as (i) "(#Hidx&#Hinv)".
@@ -38,7 +38,7 @@ Section shared_borrows.
 
   Lemma shr_borrow_acc_tok E q κ :
     ↑lftN ⊆ E →
-    lft_ctx ⊢ &shr{κ}P -∗ q.[κ] ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ q.[κ]).
+    lft_ctx -∗ &shr{κ}P -∗ q.[κ] ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ q.[κ]).
   Proof.
     iIntros (?) "#LFT #Hshr Hκ".
     iMod (shr_borrow_acc with "LFT Hshr") as "[[$ Hclose]|[H† _]]". done.
@@ -46,7 +46,7 @@ Section shared_borrows.
     - iDestruct (lft_own_dead with "Hκ H†") as "[]".
   Qed.
 
-  Lemma shr_borrow_shorten κ κ': κ ⊑ κ' ⊢ &shr{κ'}P -∗ &shr{κ}P.
+  Lemma shr_borrow_shorten κ κ': κ ⊑ κ' -∗ &shr{κ'}P -∗ &shr{κ}P.
   Proof.
     iIntros "#H⊑ H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
       by iApply (idx_borrow_shorten with "H⊑").
diff --git a/theories/tl_borrow.v b/theories/tl_borrow.v
index 7dcd10f8..3b78fb28 100644
--- a/theories/tl_borrow.v
+++ b/theories/tl_borrow.v
@@ -28,7 +28,7 @@ Section tl_borrow.
 
   Lemma tl_borrow_acc q κ E F :
     ↑lftN ⊆ E → ↑tlN ⊆ E → ↑N ⊆ F →
-    lft_ctx ⊢ &tl{κ|tid|N}P -∗ q.[κ] -∗ tl_own tid F ={E}=∗
+    lft_ctx -∗ &tl{κ|tid|N}P -∗ q.[κ] -∗ tl_own tid F ={E}=∗
             ▷P ∗ tl_own tid (F ∖ ↑N) ∗
             (▷P -∗ tl_own tid (F ∖ ↑N) ={E}=∗ q.[κ] ∗ tl_own tid F).
   Proof.
@@ -40,7 +40,7 @@ Section tl_borrow.
     iMod ("Hclose'" with "HP") as "[Hown $]". iApply "Hclose". by iFrame.
   Qed.
 
-  Lemma tl_borrow_shorten κ κ': κ ⊑ κ' ⊢ &tl{κ'|tid|N}P -∗ &tl{κ|tid|N}P.
+  Lemma tl_borrow_shorten κ κ': κ ⊑ κ' -∗ &tl{κ'|tid|N}P -∗ &tl{κ|tid|N}P.
   Proof.
     iIntros "Hκκ' H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
     iApply (idx_borrow_shorten with "Hκκ' H").
diff --git a/theories/type.v b/theories/type.v
index 9a488082..21b23768 100644
--- a/theories/type.v
+++ b/theories/type.v
@@ -30,7 +30,7 @@ Record type :=
     ty_dup_persistent tid vl : ty_dup → PersistentP (ty_own tid vl);
     ty_shr_persistent κ tid E l : PersistentP (ty_shr κ tid E l);
 
-    ty_size_eq tid vl : ty_own tid vl ⊢ ⌜length vl = ty_size⌝;
+    ty_size_eq tid vl : ty_own tid vl -∗ ⌜length vl = ty_size⌝;
     (* The mask for starting the sharing does /not/ include the
        namespace N, for allowing more flexibility for the user of
        this type (typically for the [own] type). AFAIK, there is no
@@ -41,12 +41,12 @@ Record type :=
        more consistent with thread-local tokens, which we do not
        give any. *)
     ty_share E N κ l tid q : mgmtE ⊥ ↑N → mgmtE ⊆ E →
-      lft_ctx ⊢ &{κ} (l ↦∗: ty_own tid) -∗ q.[κ] ={E}=∗ ty_shr κ tid (↑N) l ∗ q.[κ];
+      lft_ctx -∗ &{κ} (l ↦∗: ty_own tid) -∗ q.[κ] ={E}=∗ ty_shr κ tid (↑N) l ∗ q.[κ];
     ty_shr_mono κ κ' tid E E' l : E ⊆ E' →
-      lft_ctx ⊢ κ' ⊑ κ -∗ ty_shr κ tid E l -∗ ty_shr κ' tid E' l;
+      lft_ctx -∗ κ' ⊑ κ -∗ ty_shr κ tid E l -∗ ty_shr κ' tid E' l;
     ty_shr_acc κ tid E F l q :
       ty_dup → mgmtE ∪ F ⊆ E →
-      lft_ctx ⊢ ty_shr κ tid F l -∗
+      lft_ctx -∗ ty_shr κ tid F l -∗
         q.[κ] ∗ tl_own tid F ={E}=∗ ∃ q', ▷l ↦∗{q'}: ty_own tid ∗
            (▷l ↦∗{q'}: ty_own tid ={E}=∗ q.[κ] ∗ tl_own tid F)
   }.
@@ -59,7 +59,7 @@ Record simple_type `{iris_typeG Σ} :=
   { st_size : nat;
     st_own : thread_id → list val → iProp Σ;
 
-    st_size_eq tid vl : st_own tid vl ⊢ ⌜length vl = st_size⌝;
+    st_size_eq tid vl : st_own tid vl -∗ ⌜length vl = st_size⌝;
     st_own_persistent tid vl : PersistentP (st_own tid vl) }.
 Global Existing Instance st_own_persistent.
 
@@ -244,10 +244,10 @@ Section types.
   Qed.
   Next Obligation.
     intros κ0 ty κ κ' tid E E' l ?. iIntros "#LFT #Hκ #H".
-    iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0⋅κ' ⊑ κ0⋅κ) as "#Hκ0".
-    { iApply lft_incl_lb. iSplit.
+    iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0⋅κ' ⊑ κ0⋅κ)%I as "#Hκ0".
+    { iApply (lft_incl_lb with "[] []").
       - iApply lft_le_incl. by exists κ'.
-      - iApply lft_incl_trans. iSplit; last done.
+      - iApply (lft_incl_trans with "[] Hκ").
         iApply lft_le_incl. exists κ0. apply (comm _). }
     iExists l'. iSplit. by iApply (frac_borrow_shorten with "[]"). iIntros (q) "!#Htok".
     iApply step_fupd_mask_mono. reflexivity. apply union_preserving_l. eassumption.
@@ -368,7 +368,7 @@ Section types.
   Proof. intros. constructor; done. Qed.
 
   Lemma sum_size_eq n tid i tyl vl {Hn : LstTySize n tyl} :
-    ty_own (nth i tyl emp) tid vl ⊢ ⌜length vl = n⌝.
+    ty_own (nth i tyl emp) tid vl -∗ ⌜length vl = n⌝.
   Proof.
     iIntros "Hown". iDestruct (ty_size_eq with "Hown") as %->.
     revert Hn. rewrite /LstTySize List.Forall_forall /= =>Hn.
diff --git a/theories/type_incl.v b/theories/type_incl.v
index a7f34971..8ce12186 100644
--- a/theories/type_incl.v
+++ b/theories/type_incl.v
@@ -9,7 +9,7 @@ Section ty_incl.
   Context `{iris_typeG Σ}.
 
   Definition ty_incl (ρ : perm) (ty1 ty2 : type) :=
-    ∀ tid, lft_ctx ⊢ ρ tid ={⊤}=∗
+    ∀ tid, lft_ctx -∗ ρ tid ={⊤}=∗
       (□ ∀ vl, ty1.(ty_own) tid vl → ty2.(ty_own) tid vl) ∗
       (□ ∀ κ E l, ty1.(ty_shr) κ tid E l →
        (* [ty_incl] needs to prove something about the length of the
@@ -19,7 +19,7 @@ Section ty_incl.
                   ty2.(ty_shr) κ tid E l ∗ ⌜ty1.(ty_size) = ty2.(ty_size)⌝).
 
   Global Instance ty_incl_refl ρ : Reflexive (ty_incl ρ).
-  Proof. iIntros (ty tid) "__!>". iSplit; iIntros "!#"; eauto. Qed.
+  Proof. iIntros (ty tid) "_ _!>". iSplit; iIntros "!#"; eauto. Qed.
 
   Lemma ty_incl_trans ρ θ ty1 ty2 ty3 :
     ty_incl ρ ty1 ty2 → ty_incl θ ty2 ty3 → ty_incl (ρ ∗ θ) ty1 ty3.
@@ -74,10 +74,9 @@ Section ty_incl.
     iIntros (tid) "#LFT #Hincl!>". iSplit; iIntros "!#*H".
     - iDestruct "H" as (l) "[% Hown]". subst. iExists _. iSplit. done.
       by iApply (borrow_shorten with "Hincl").
-    - iAssert (κ1 ⋅ κ ⊑ κ2 ⋅ κ) as "#Hincl'".
-      { iApply lft_incl_lb. iSplit.
-        - iApply lft_incl_trans. iSplit; last done.
-          iApply lft_le_incl. by exists κ.
+    - iAssert (κ1 ⋅ κ ⊑ κ2 ⋅ κ)%I as "#Hincl'".
+      { iApply (lft_incl_lb with "[] []").
+        - iApply (lft_incl_trans with "[] Hincl"). iApply lft_le_incl. by exists κ.
         - iApply lft_le_incl. exists κ1. by apply (comm _). }
       iSplitL; last done. iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'.
       iFrame. iIntros (q') "!#Htok".
@@ -191,7 +190,7 @@ Section ty_incl.
     ty_incl ρ (sum tyl1) (sum tyl2).
   Proof.
     iIntros (DUP FA tid) "#LFT #Hρ". rewrite /sum /=. iSplitR "".
-    - assert (Hincl : lft_ctx ⊢ ρ tid ={⊤}=∗
+    - assert (Hincl : lft_ctx -∗ ρ tid ={⊤}=∗
          (□ ∀ i vl, (nth i tyl1 ∅%T).(ty_own) tid vl
                   → (nth i tyl2 ∅%T).(ty_own) tid vl)).
       { clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
@@ -202,7 +201,7 @@ Section ty_incl.
       iMod (Hincl with "LFT Hρ") as "#Hincl". iIntros "!>!#*H".
       iDestruct "H" as (i vl') "[% Hown]". subst. iExists _, _. iSplit. done.
         by iApply "Hincl".
-    - assert (Hincl : lft_ctx ⊢ ρ tid ={⊤}=∗
+    - assert (Hincl : lft_ctx -∗ ρ tid ={⊤}=∗
          (□ ∀ i κ E l, (nth i tyl1 ∅%T).(ty_shr) κ tid E l
                      → (nth i tyl2 ∅%T).(ty_shr) κ tid E l)).
       { clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
diff --git a/theories/typing.v b/theories/typing.v
index a50ed406..4ba6d657 100644
--- a/theories/typing.v
+++ b/theories/typing.v
@@ -87,7 +87,7 @@ Section typing.
   Lemma typed_valuable (ν : expr) ty:
     typed_step_ty (ν ◁ ty) ν ty.
   Proof.
-    iIntros (tid) "!#(_&_&H&$)". iApply (has_type_wp with "[$H]"). by iIntros (v) "[_$]".
+    iIntros (tid) "!#(_&_&H&$)". iApply (has_type_wp with "[$H]"). by iIntros (v) "_ $".
   Qed.
 
   Lemma typed_plus e1 e2 ρ1 ρ2:
@@ -165,7 +165,7 @@ Section typing.
     typed_step (ν ◁ own 1 ty) (Free #ty.(ty_size) ν) (λ _, top).
   Proof.
     iIntros (tid) "!#(#HEAP&_&H◁&$)". wp_bind ν.
-    iApply (has_type_wp with "[$H◁]"). iIntros (v) "[_ H◁]!>".
+    iApply (has_type_wp with "[$H◁]"). iIntros (v) "_ H◁ !>".
     rewrite has_type_value.
     iDestruct "H◁" as (l) "(Hv & H↦∗: & >H†)". iDestruct "Hv" as %[=->].
     iDestruct "H↦∗:" as (vl) "[>H↦ Hown]".
@@ -174,7 +174,7 @@ Section typing.
 
   Definition consumes (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
     ∀ ν tid Φ E, mgmtE ∪ ↑lrustN ⊆ E →
-      lft_ctx ⊢ ρ1 ν tid -∗ tl_own tid ⊤ -∗
+      lft_ctx -∗ ρ1 ν tid -∗ tl_own tid ⊤ -∗
       (∀ (l:loc) vl q,
         (⌜length vl = ty.(ty_size)⌝ ∗ ⌜eval_expr ν = Some #l⌝ ∗ l ↦∗{q} vl ∗
          |={E}▷=> (ty.(ty_own) tid vl ∗ (l ↦∗{q} vl ={E}=∗ ρ2 ν tid ∗ tl_own tid ⊤)))
@@ -184,8 +184,8 @@ Section typing.
   Lemma consumes_copy_own ty q:
     ty.(ty_dup) → consumes ty (λ ν, ν ◁ own q ty)%P (λ ν, ν ◁ own q ty)%P.
   Proof.
-    iIntros (? ν tid Φ E ?) "_ H◁ Htl HΦ". iApply (has_type_wp with "[- $H◁]").
-    iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
+    iIntros (? ν tid Φ E ?) "_ H◁ Htl HΦ". iApply (has_type_wp with "H◁").
+    iIntros (v) "Hνv H◁". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & H↦ & >H†)".
     iDestruct "Heq" as %[=->]. iDestruct "H↦" as (vl) "[>H↦ #Hown]".
     iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">%".
@@ -198,8 +198,8 @@ Section typing.
     consumes ty (λ ν, ν ◁ own q ty)%P
              (λ ν, ν ◁ own q (Π(replicate ty.(ty_size) uninit)))%P.
   Proof.
-    iIntros (ν tid Φ E ?) "_ H◁ Htl HΦ". iApply (has_type_wp with "[- $H◁]").
-    iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
+    iIntros (ν tid Φ E ?) "_ H◁ Htl HΦ". iApply (has_type_wp with "H◁").
+    iIntros (v) "Hνv H◁". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & H↦ & >H†)".
     iDestruct "Heq" as %[=->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
     iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">Hlen".
@@ -219,7 +219,7 @@ Section typing.
                 (λ ν, ν ◁ &uniq{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
   Proof.
     iIntros (? ν tid Φ E ?) "#LFT (H◁ & #H⊑ & Htok) Htl HΦ".
-    iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
+    iApply (has_type_wp with "H◁"). iIntros (v) "Hνv H◁". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l') "[Heq H↦]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
     iMod (borrow_acc with "LFT H↦ Htok") as "[H↦ Hclose']". set_solver.
@@ -237,7 +237,7 @@ Section typing.
                 (λ ν, ν ◁ &shr{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
   Proof.
     iIntros (? ν tid Φ E ?) "#LFT (H◁ & #H⊑ & Htok) Htl HΦ".
-    iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
+    iApply (has_type_wp with "H◁"). iIntros (v) "Hνv H◁". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l') "[Heq #Hshr]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
     rewrite (union_difference_L (↑lrustN) ⊤); last done.
@@ -268,7 +268,7 @@ Section typing.
                (λ v, v ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
   Proof.
     iIntros (tid) "!#(#HEAP & #LFT & (H◁ & #H⊑ & Htok) & $)". wp_bind ν.
-    iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
+    iApply (has_type_wp with "H◁"). iIntros (v) "Hνv H◁!>". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "[Heq H↦]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[Htok Hclose]". done.
     iMod (borrow_acc_strong with "LFT H↦ Htok") as "[H↦ Hclose']". done.
@@ -288,7 +288,7 @@ Section typing.
                (λ v, v ◁ &shr{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
   Proof.
     iIntros (tid) "!#(#HEAP & #LFT & (H◁ & #H⊑ & Htok) & $)". wp_bind ν.
-    iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
+    iApply (has_type_wp with "H◁"). iIntros (v) "Hνv H◁!>". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "[Heq #H↦]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[[Htok1 Htok2] Hclose]". done.
     iDestruct "H↦" as (vl) "[H↦b Hown]".
@@ -311,7 +311,7 @@ Section typing.
                (λ v, v ◁ &uniq{κ'} ty ∗ κ ⊑ κ' ∗ q.[κ])%P.
   Proof.
     iIntros (tid) "!#(#HEAP & #LFT & (H◁ & #H⊑1 & Htok & #H⊑2) & $)". wp_bind ν.
-    iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
+    iApply (has_type_wp with "H◁"). iIntros (v) "Hνv H◁!>". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "[Heq H↦]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_acc with "H⊑1 Htok") as (q'') "[Htok Hclose]". done.
     iMod (borrow_exists with "LFT H↦") as (vl) "Hbor". done.
@@ -329,7 +329,7 @@ Section typing.
       iMod ("Hclose'" with "[$H↦]") as "[H↦ Htok]".
       iMod ("Hclose" with "Htok") as "$". iFrame "#".
       iExists _. iSplitR. done. iApply (borrow_shorten with "[] Hbor").
-      iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl.
+      iApply (lft_incl_lb with "H⊑2"). iApply lft_incl_refl.
   Qed.
 
   Lemma typed_deref_shr_borrow_borrow ty ν κ κ' κ'' q:
@@ -338,13 +338,13 @@ Section typing.
                (λ v, v ◁ &shr{κ'} ty ∗ κ ⊑ κ' ∗ q.[κ])%P.
   Proof.
     iIntros (tid) "!#(#HEAP & #LFT & (H◁ & #H⊑1 & Htok & #H⊑2) & $)". wp_bind ν.
-    iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
+    iApply (has_type_wp with "H◁"). iIntros (v) "Hνv H◁!>". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "[Heq Hshr]".
     iDestruct "Heq" as %[=->]. iDestruct "Hshr" as (l') "[H↦ Hown]".
     iMod (lft_incl_acc with "H⊑1 Htok") as (q') "[[Htok1 Htok2] Hclose]". done.
     iMod (frac_borrow_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
-    iAssert (κ' ⊑ κ'' ⋅ κ') as "#H⊑3".
-    { iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl. }
+    iAssert (κ' ⊑ κ'' ⋅ κ')%I as "#H⊑3".
+    { iApply (lft_incl_lb with "H⊑2 []"). iApply lft_incl_refl. }
     iMod (lft_incl_acc with "H⊑3 Htok2") as (q''') "[Htok Hclose'']". done.
     iSpecialize ("Hown" $! _ with "Htok").
     iApply wp_strong_mono. reflexivity. iSplitL "Hclose Hclose' Hclose''"; last first.
@@ -361,19 +361,18 @@ Section typing.
 
   Definition update (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
     ∀ ν tid Φ E, mgmtE ∪ (↑lrustN) ⊆ E →
-      lft_ctx ⊢ ρ1 ν tid -∗
+      lft_ctx -∗ ρ1 ν tid -∗
       (∀ (l:loc) vl,
          (⌜length vl = ty.(ty_size)⌝ ∗ ⌜eval_expr ν = Some #l⌝ ∗ l ↦∗ vl ∗
-         ∀ vl', l ↦∗ vl' ∗ ▷ (ty.(ty_own) tid vl') ={E}=∗ ρ2 ν tid)
-         -∗ Φ #l)
-      -∗ WP ν @ E {{ Φ }}.
+           ∀ vl', l ↦∗ vl' ∗ ▷ (ty.(ty_own) tid vl') ={E}=∗ ρ2 ν tid) -∗ Φ #l) -∗
+      WP ν @ E {{ Φ }}.
 
   Lemma update_strong ty1 ty2 q:
     ty1.(ty_size) = ty2.(ty_size) →
     update ty1 (λ ν, ν ◁ own q ty2)%P (λ ν, ν ◁ own q ty1)%P.
   Proof.
-    iIntros (Hsz ν tid Φ E ?) "_ H◁ HΦ". iApply (has_type_wp with "[- $H◁]").
-    iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
+    iIntros (Hsz ν tid Φ E ?) "_ H◁ HΦ". iApply (has_type_wp with "H◁").
+    iIntros (v) "Hνv H◁". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & H↦ & >H†)".
     iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
     rewrite ty2.(ty_size_eq) -Hsz. iDestruct "Hown" as ">%". iApply "HΦ". iFrame "∗%".
@@ -386,7 +385,7 @@ Section typing.
               (λ ν, ν ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
   Proof.
     iIntros (ν tid Φ E ?) "#LFT (H◁ & #H⊑ & Htok) HΦ".
-    iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
+    iApply (has_type_wp with "H◁"). iIntros (v) "Hνv H◁". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & H↦)". iDestruct "Heq" as %[=->].
     iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
     iMod (borrow_acc with "LFT H↦ Htok") as "[H↦ Hclose']". set_solver.
@@ -403,7 +402,7 @@ Section typing.
     iIntros (Hsz Hupd tid) "!#(#HEAP & #LFT & [Hρ1 H◁] & $)". wp_bind ν1.
     iApply (Hupd with "LFT Hρ1"). done. iFrame. iIntros (l vl) "(%&%&H↦&Hupd)".
     rewrite ->Hsz in *. destruct vl as [|v[|]]; try done.
-    wp_bind ν2. iApply (has_type_wp with "[- $H◁]"). iIntros (v') "[% H◁]!>".
+    wp_bind ν2. iApply (has_type_wp with "H◁"). iIntros (v') "% H◁!>".
     rewrite heap_mapsto_vec_singleton. wp_write.
     rewrite -heap_mapsto_vec_singleton has_type_value. iApply "Hupd". by iFrame.
   Qed.
@@ -452,7 +451,7 @@ Section typing.
     typed_program (ρ ∗ ν ◁ bool) (if: ν then e1 else e2).
   Proof.
     iIntros (He1 He2 tid) "!#(#HEAP & #LFT & [Hρ H◁] & Htl)".
-    wp_bind ν. iApply has_type_wp. iFrame. iIntros (v) "[% H◁]!>".
+    wp_bind ν. iApply (has_type_wp with "H◁"). iIntros (v) "% H◁!>".
     rewrite has_type_value. iDestruct "H◁" as (b) "Heq". iDestruct "Heq" as %[= ->].
     wp_if. destruct b; iNext. iApply He1; iFrame "∗#". iApply He2; iFrame "∗#".
   Qed.
-- 
GitLab