diff --git a/theories/lifetime/borrow.v b/theories/lifetime/borrow.v
index b169837ac1df533ae1f2f70bf68b21d19e58a0d7..711a701e44916431d7fa3620ac60707c3065308b 100644
--- a/theories/lifetime/borrow.v
+++ b/theories/lifetime/borrow.v
@@ -17,11 +17,11 @@ Qed.
 Lemma bor_shorten κ κ' P: κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
 Proof.
   unfold bor. iIntros "#Hκκ' H". iDestruct "H" as (i) "[#? ?]".
-  iExists i. iFrame. iApply lft_incl_trans. eauto.
+  iExists i. iFrame. by iApply (lft_incl_trans with "Hκκ'").
 Qed.
 
 Lemma idx_bor_shorten κ κ' i P : κ ⊑ κ' -∗ &{κ',i} P -∗ &{κ,i} P.
-Proof. unfold idx_bor. iIntros "#Hκκ' [#? $]". iApply lft_incl_trans. eauto. Qed.
+Proof. unfold idx_bor. iIntros "#Hκκ' [#? $]". by iApply (lft_incl_trans with "Hκκ'"). Qed.
 
 Lemma bor_fake_internal E κ P :
   ↑borN ⊆ E →
@@ -41,7 +41,7 @@ Qed.
 
 Lemma bor_fake E κ P :
   ↑lftN ⊆ E →
-  lft_ctx ⊢ [†κ] ={E}=∗ &{κ}P.
+  lft_ctx -∗ [†κ] ={E}=∗ &{κ}P.
 Proof.
   iIntros (?) "#Hmgmt H†". iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
   iMod (ilft_create _ _ κ with "HI HA Hinv") as (A' I') "(Hκ & HI & HA & Hinv)".
diff --git a/theories/lifetime/derived.v b/theories/lifetime/derived.v
index 689aa4eeb57db243d7d9e338ae266eb16edf48cf..84daca8e85791a4f185a91ac892b3bf35d08fc7d 100644
--- a/theories/lifetime/derived.v
+++ b/theories/lifetime/derived.v
@@ -8,7 +8,7 @@ Implicit Types κ : lft.
 (*** Derived lemmas  *)
 Lemma bor_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 (bor_acc_strong with "LFT HP Htok") as "[HP Hclose]"; first done.
@@ -17,7 +17,7 @@ Qed.
 
 Lemma bor_exists {A} (Φ : A → iProp Σ) `{!Inhabited A} E κ :
   ↑lftN ⊆ E →
-  lft_ctx ⊢ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
+  lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
 Proof.
   iIntros (?) "#LFT Hb".
   iMod (bor_acc_atomic_strong with "LFT Hb") as "[[HΦ Hclose]|[H† Hclose]]"; first done.
@@ -28,7 +28,7 @@ Qed.
 
 Lemma bor_or E κ P Q :
   ↑lftN ⊆ E →
-  lft_ctx ⊢ &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q).
+  lft_ctx -∗ &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q).
 Proof.
   iIntros (?) "#LFT H". rewrite uPred.or_alt.
   iMod (bor_exists with "LFT H") as ([]) "H"; auto.
@@ -36,7 +36,7 @@ Qed.
 
 Lemma bor_persistent `{!PersistentP P} E κ q :
   ↑lftN ⊆ E →
-  lft_ctx ⊢ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
+  lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
 Proof.
   iIntros (?) "#LFT Hb Htok".
   iMod (bor_acc with "LFT Hb Htok") as "[#HP Hob]"; first done.
@@ -45,7 +45,7 @@ Qed.
 
 Lemma lft_incl_acc E κ κ' q :
   ↑lftN ⊆ E →
-  κ ⊑ κ' ⊢ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
+  κ ⊑ κ' -∗ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
 Proof.
   rewrite /lft_incl.
   iIntros (?) "#[H _] Hq". iApply fupd_mask_mono; first done.
@@ -53,13 +53,13 @@ Proof.
   iIntros "{$Hq'} !> Hq". iApply fupd_mask_mono; first done. by iApply "Hclose".
 Qed.
 
-Lemma lft_incl_dead E κ κ' : ↑lftN ⊆ E → κ ⊑ κ' ⊢ [†κ'] ={E}=∗ [†κ].
+Lemma lft_incl_dead E κ κ' : ↑lftN ⊆ E → κ ⊑ κ' -∗ [†κ'] ={E}=∗ [†κ].
 Proof.
   rewrite /lft_incl.
   iIntros (?) "#[_ H] Hq". iApply fupd_mask_mono; first done. by iApply "H".
 Qed.
 
-Lemma lft_incl_lb κ κ' κ'' : κ ⊑ κ' ∗ κ ⊑ κ'' ⊢ κ ⊑ κ' ∪ κ''.
+Lemma lft_incl_lb κ κ' κ'' : κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ∪ κ''.
 Proof. (*
   iIntros "[#[H1 H1†] #[H2 H2†]]!#". iSplitR.
   - iIntros (q) "[Hκ'1 Hκ'2]".
@@ -74,7 +74,7 @@ Proof. (*
   - rewrite -lft_dead_or. iIntros "[H†|H†]". by iApply "H1†". by iApply "H2†".
 Qed. *) Admitted.
 
-Lemma lft_incl_static κ : True ⊢ κ ⊑ static.
+Lemma lft_incl_static κ : (κ ⊑ static)%I.
 Proof.
   iIntros "!#". iSplitR.
   - iIntros (q) "?". iExists 1%Qp. iSplitR. by iApply lft_tok_static. auto.
@@ -83,7 +83,7 @@ Qed.
 
 Lemma reborrow E P κ κ' :
   ↑lftN ⊆ E →
-  lft_ctx ⊢ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗  &{κ}P).
+  lft_ctx -∗ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗  &{κ}P).
 Proof.
   iIntros (?) "#LFT #H⊑ HP". (* iMod (bor_rebor' with "LFT HP") as "[Hκ' H∋]".
     done. by exists κ'.
diff --git a/theories/lifetime/primitive.v b/theories/lifetime/primitive.v
index 7fff56c7ca462652f6d5fa9348cc2dc79664c6a1..f10c73b23eb67e71bfb92089f638dab3fd60a052 100644
--- a/theories/lifetime/primitive.v
+++ b/theories/lifetime/primitive.v
@@ -19,7 +19,7 @@ Qed.
 
 (** Ownership *)
 Lemma own_ilft_auth_agree (I : gmap lft lft_names) κ γs :
-  own_ilft_auth I ⊢
+  own_ilft_auth I -∗
     own ilft_name (◯ {[κ := DecAgree γs]}) -∗ ⌜is_Some (I !! κ)⌝.
 Proof.
   iIntros "HI Hκ". iDestruct (own_valid_2 with "HI Hκ")
@@ -28,7 +28,7 @@ Proof.
 Qed.
 
 Lemma own_alft_auth_agree (A : gmap atomic_lft bool) Λ b :
-  own_alft_auth A ⊢
+  own_alft_auth A -∗
     own alft_name (◯ {[Λ := to_lft_stateR b]}) -∗ ⌜A !! Λ = Some b⌝.
 Proof.
   iIntros "HA HΛ".
@@ -38,7 +38,7 @@ Proof.
   move=> [/leibniz_equiv_iff|/csum_included]; destruct b, b'; naive_solver.
 Qed.
 
-Lemma own_bor_auth I κ x : own_ilft_auth I ⊢ own_bor κ x -∗ ⌜is_Some (I !! κ)⌝.
+Lemma own_bor_auth I κ x : own_ilft_auth I -∗ own_bor κ x -∗ ⌜is_Some (I !! κ)⌝.
 Proof.
   iIntros "HI"; iDestruct 1 as (γs) "[? _]".
   by iApply (own_ilft_auth_agree with "HI").
@@ -53,16 +53,16 @@ Proof.
   move: Hγs; rewrite /= op_singleton singleton_valid=> /dec_agree_op_inv [<-].
   iExists γs. iSplit. done. rewrite own_op; iFrame.
 Qed.
-Lemma own_bor_valid κ x : own_bor κ x ⊢ ✓ x.
+Lemma own_bor_valid κ x : own_bor κ x -∗ ✓ x.
 Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
-Lemma own_bor_valid_2 κ x y : own_bor κ x ⊢ own_bor κ y -∗ ✓ (x ⋅ y).
+Lemma own_bor_valid_2 κ x y : own_bor κ x -∗ own_bor κ y -∗ ✓ (x ⋅ y).
 Proof. apply wand_intro_r. rewrite -own_bor_op. apply own_bor_valid. Qed.
 Lemma own_bor_update κ x y : x ~~> y → own_bor κ x ==∗ own_bor κ y.
 Proof.
   iDestruct 1 as (γs) "[#Hκ Hx]"; iExists γs. iFrame "Hκ". by iApply own_update.
 Qed.
 
-Lemma own_cnt_auth I κ x : own_ilft_auth I ⊢ own_cnt κ x -∗ ⌜is_Some (I !! κ)⌝.
+Lemma own_cnt_auth I κ x : own_ilft_auth I -∗ own_cnt κ x -∗ ⌜is_Some (I !! κ)⌝.
 Proof.
   iIntros "HI"; iDestruct 1 as (γs) "[? _]".
   by iApply (own_ilft_auth_agree with "HI").
@@ -77,21 +77,21 @@ Proof.
   move: Hγs; rewrite /= op_singleton singleton_valid=> /dec_agree_op_inv [<-].
   iExists γs. iSplit; first done. rewrite own_op; iFrame.
 Qed.
-Lemma own_cnt_valid κ x : own_cnt κ x ⊢ ✓ x.
+Lemma own_cnt_valid κ x : own_cnt κ x -∗ ✓ x.
 Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
-Lemma own_cnt_valid_2 κ x y : own_cnt κ x ⊢ own_cnt κ y -∗ ✓ (x ⋅ y).
+Lemma own_cnt_valid_2 κ x y : own_cnt κ x -∗ own_cnt κ y -∗ ✓ (x ⋅ y).
 Proof. apply wand_intro_r. rewrite -own_cnt_op. apply own_cnt_valid. Qed.
 Lemma own_cnt_update κ x y : x ~~> y → own_cnt κ x ==∗ own_cnt κ y.
 Proof.
   iDestruct 1 as (γs) "[#Hκ Hx]"; iExists γs. iFrame "Hκ". by iApply own_update.
 Qed.
 Lemma own_cnt_update_2 κ x1 x2 y :
-  x1 ⋅ x2 ~~> y → own_cnt κ x1 ⊢ own_cnt κ x2 ==∗ own_cnt κ y.
+  x1 ⋅ x2 ~~> y → own_cnt κ x1 -∗ own_cnt κ x2 ==∗ own_cnt κ y.
 Proof.
   intros. apply wand_intro_r. rewrite -own_cnt_op. by apply own_cnt_update.
 Qed.
 
-Lemma own_inh_auth I κ x : own_ilft_auth I ⊢ own_inh κ x -∗ ⌜is_Some (I !! κ)⌝.
+Lemma own_inh_auth I κ x : own_ilft_auth I -∗ own_inh κ x -∗ ⌜is_Some (I !! κ)⌝.
 Proof.
   iIntros "HI"; iDestruct 1 as (γs) "[? _]".
   by iApply (own_ilft_auth_agree with "HI").
@@ -106,9 +106,9 @@ Proof.
   move: Hγs; rewrite /= op_singleton singleton_valid=> /dec_agree_op_inv [<-].
   iExists γs. iSplit. done. rewrite own_op; iFrame.
 Qed.
-Lemma own_inh_valid κ x : own_inh κ x ⊢ ✓ x.
+Lemma own_inh_valid κ x : own_inh κ x -∗ ✓ x.
 Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
-Lemma own_inh_valid_2 κ x y : own_inh κ x ⊢ own_inh κ y -∗ ✓ (x ⋅ y).
+Lemma own_inh_valid_2 κ x y : own_inh κ x -∗ own_inh κ y -∗ ✓ (x ⋅ y).
 Proof. apply wand_intro_r. rewrite -own_inh_op. apply own_inh_valid. Qed.
 Lemma own_inh_update κ x y : x ~~> y → own_inh κ x ==∗ own_inh κ y.
 Proof.
@@ -178,7 +178,7 @@ Qed.
 Lemma lft_dead_in_insert_false' A κ Λ : Λ ∈ κ → lft_dead_in (<[Λ:=false]> A) κ.
 Proof. exists Λ. by rewrite lookup_insert. Qed.
 
-Lemma lft_inv_alive_twice κ : lft_inv_alive κ ⊢ lft_inv_alive κ -∗ False.
+Lemma lft_inv_alive_twice κ : lft_inv_alive κ -∗ lft_inv_alive κ -∗ False.
 Proof.
   rewrite lft_inv_alive_unfold /lft_inh.
   iDestruct 1 as (P Q) "(_&_&Hinh)"; iDestruct 1 as (P' Q') "(_&_&Hinh')".
@@ -216,7 +216,7 @@ Qed.
 Lemma lft_tok_split κ q : q.[κ] ⊣⊢ (q/2).[κ] ∗ (q/2).[κ].
 Proof. by rewrite -lft_tok_frac_op Qp_div_2. Qed.
 
-Lemma lft_tok_dead_own q κ : q.[κ] ⊢ [† κ] -∗ False.
+Lemma lft_tok_dead_own q κ : q.[κ] -∗ [† κ] -∗ False.
 Proof.
   rewrite /lft_tok /lft_dead. iIntros "H"; iDestruct 1 as (Λ') "[% H']".
   iDestruct (big_sepMS_elem_of _ _ Λ' with "H") as "H"=> //.
@@ -224,14 +224,14 @@ Proof.
   move: Hvalid=> /auth_own_valid /=; by rewrite op_singleton singleton_valid.
 Qed.
 
-Lemma lft_tok_static q : True ⊢ q.[static].
+Lemma lft_tok_static q : q.[static]%I.
 Proof. by rewrite /lft_tok big_sepMS_empty. Qed.
 
-Lemma lft_dead_static : [† static] ⊢ False.
+Lemma lft_dead_static : [† static] -∗ False.
 Proof. rewrite /lft_dead. iDestruct 1 as (Λ) "[% H']". set_solver. Qed.
 
 (** Lifetime inclusion *)
-Lemma lft_le_incl κ κ' : κ' ⊆ κ → True ⊢ κ ⊑ κ'.
+Lemma lft_le_incl κ κ' : κ' ⊆ κ → (κ ⊑ κ')%I.
 Proof.
   iIntros (->%gmultiset_union_difference) "!#". iSplitR.
   - iIntros (q). rewrite <-lft_tok_op. iIntros "[H Hf]". iExists q. iFrame.
@@ -239,12 +239,12 @@ Proof.
   - 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.
-  rewrite /lft_incl. iIntros "[#[H1 H1†] #[H2 H2†]] !#". iSplitR.
+  rewrite /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']".
diff --git a/theories/lifetime/rebor.v b/theories/lifetime/rebor.v
index f28263c6cbe54dc2ea846ac58daf1b2d3b06b63d..3f428237c2ed23c297349217621480ecbb0ea503 100644
--- a/theories/lifetime/rebor.v
+++ b/theories/lifetime/rebor.v
@@ -10,7 +10,7 @@ Implicit Types κ : lft.
 
 Lemma bor_fake E κ P :
   ↑lftN ⊆ E →
-  lft_ctx ⊢ [†κ] ={E}=∗ &{κ}P.
+  lft_ctx -∗ [†κ] ={E}=∗ &{κ}P.
 Proof.
 Admitted.
 
@@ -51,10 +51,10 @@ Admitted.
 
 Lemma bor_rebor' E κ κ' P :
   ↑lftN ⊆ E → κ ⊆ κ' →
-  lft_ctx ⊢ &{κ} P ={E}=∗ &{κ'} P ∗ ([†κ'] ={E}=∗ &{κ} P).
+  lft_ctx -∗ &{κ} P ={E}=∗ &{κ'} P ∗ ([†κ'] ={E}=∗ &{κ} P).
 Proof. Admitted.
 Lemma bor_unnest E κ κ' P :
   ↑lftN ⊆ E →
-  lft_ctx ⊢ &{κ'} &{κ} P ={E}▷=∗ &{κ ∪ κ'} P.
+  lft_ctx -∗ &{κ'} &{κ} P ={E}▷=∗ &{κ ∪ κ'} P.
 Proof. Admitted.
 End rebor.
\ No newline at end of file