diff --git a/base_logic/big_op.v b/base_logic/big_op.v
index be9ae4df854446d2b7b6963d8a3d301e62043a33..f47cab4de2b0855fbdbc1180e28bded8987245a8 100644
--- a/base_logic/big_op.v
+++ b/base_logic/big_op.v
@@ -8,13 +8,13 @@ CMRA structure on uPred. *)
 Section cmra.
   Context {M : ucmraT}.
 
-  Instance uPred_valid : Valid (uPred M) := λ P, ∀ n x, ✓{n} x → P n x.
-  Instance uPred_validN : ValidN (uPred M) := λ n P,
+  Instance uPred_valid_inst : Valid (uPred M) := λ P, ∀ n x, ✓{n} x → P n x.
+  Instance uPred_validN_inst : ValidN (uPred M) := λ n P,
     ∀ n' x, n' ≤ n → ✓{n'} x → P n' x.
   Instance uPred_op : Op (uPred M) := uPred_sep.
   Instance uPred_pcore : PCore (uPred M) := λ _, Some True%I.
 
-  Instance uPred_validN_ne n : Proper (dist n ==> iff) (uPred_validN n).
+  Instance uPred_validN_ne n : Proper (dist n ==> iff) (uPred_validN_inst n).
   Proof. intros P Q HPQ; split=> H n' x ??; by apply HPQ, H. Qed.
 
   Lemma uPred_validN_alt n (P : uPred M) : ✓{n} P → P ≡{n}≡ True%I.
@@ -467,7 +467,7 @@ Section gset.
   Proof. apply: big_opS_delete. Qed.
 
   Lemma big_sepS_elem_of Φ X x : x ∈ X → ([∗ set] y ∈ X, Φ y) ⊢ Φ x.
-  Proof. intros. apply uPred_included. by apply: big_opS_elem_of. Qed. 
+  Proof. intros. apply uPred_included. by apply: big_opS_elem_of. Qed.
 
   Lemma big_sepS_singleton Φ x : ([∗ set] y ∈ {[ x ]}, Φ y) ⊣⊢ Φ x.
   Proof. apply: big_opS_singleton. Qed.
diff --git a/base_logic/derived.v b/base_logic/derived.v
index 55b62ca274a671b67bd3d27bace614cab70bc795..998df1b945c42f4c01fdf1539ffbb415cc017026 100644
--- a/base_logic/derived.v
+++ b/base_logic/derived.v
@@ -67,10 +67,10 @@ Lemma impl_elim_l' P Q R : (P ⊢ Q → R) → P ∧ Q ⊢ R.
 Proof. intros; apply impl_elim with Q; auto. Qed.
 Lemma impl_elim_r' P Q R : (Q ⊢ P → R) → P ∧ Q ⊢ R.
 Proof. intros; apply impl_elim with P; auto. Qed.
-Lemma impl_entails P Q : (True ⊢ P → Q) → P ⊢ Q.
+Lemma impl_entails P Q : (P → Q)%I → P ⊢ Q.
 Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed.
-Lemma entails_impl P Q : (P ⊢ Q) → True ⊢ P → Q.
-Proof. auto using impl_intro_l. Qed.
+Lemma entails_impl P Q : (P ⊢ Q) → (P → Q)%I.
+Proof. intro. apply impl_intro_l. auto. Qed.
 
 Lemma and_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∧ P' ⊢ Q ∧ Q'.
 Proof. auto. Qed.
@@ -308,12 +308,12 @@ Global Instance iff_proper :
 
 Lemma iff_refl Q P : Q ⊢ P ↔ P.
 Proof. rewrite /uPred_iff; apply and_intro; apply impl_intro_l; auto. Qed.
-Lemma iff_equiv P Q : (True ⊢ P ↔ Q) → (P ⊣⊢ Q).
+Lemma iff_equiv P Q : (P ↔ Q)%I → (P ⊣⊢ Q).
 Proof.
   intros HPQ; apply (anti_symm (⊢));
-    apply impl_entails; rewrite HPQ /uPred_iff; auto.
+    apply impl_entails; rewrite /uPred_valid HPQ /uPred_iff; auto.
 Qed.
-Lemma equiv_iff P Q : (P ⊣⊢ Q) → True ⊢ P ↔ Q.
+Lemma equiv_iff P Q : (P ⊣⊢ Q) → (P ↔ Q)%I.
 Proof. intros ->; apply iff_refl. Qed.
 Lemma internal_eq_iff P Q : P ≡ Q ⊢ P ↔ Q.
 Proof.
@@ -362,13 +362,13 @@ Proof. intros ->; apply sep_elim_l. Qed.
 Lemma sep_elim_r' P Q R : (Q ⊢ R) → P ∗ Q ⊢ R.
 Proof. intros ->; apply sep_elim_r. Qed.
 Hint Resolve sep_elim_l' sep_elim_r'.
-Lemma sep_intro_True_l P Q R : (True ⊢ P) → (R ⊢ Q) → R ⊢ P ∗ Q.
+Lemma sep_intro_True_l P Q R : P%I → (R ⊢ Q) → R ⊢ P ∗ Q.
 Proof. by intros; rewrite -(left_id True%I uPred_sep R); apply sep_mono. Qed.
-Lemma sep_intro_True_r P Q R : (R ⊢ P) → (True ⊢ Q) → R ⊢ P ∗ Q.
+Lemma sep_intro_True_r P Q R : (R ⊢ P) → Q%I → R ⊢ P ∗ Q.
 Proof. by intros; rewrite -(right_id True%I uPred_sep R); apply sep_mono. Qed.
-Lemma sep_elim_True_l P Q R : (True ⊢ P) → (P ∗ R ⊢ Q) → R ⊢ Q.
+Lemma sep_elim_True_l P Q R : P → (P ∗ R ⊢ Q) → R ⊢ Q.
 Proof. by intros HP; rewrite -HP left_id. Qed.
-Lemma sep_elim_True_r P Q R : (True ⊢ P) → (R ∗ P ⊢ Q) → R ⊢ Q.
+Lemma sep_elim_True_r P Q R : P → (R ∗ P ⊢ Q) → R ⊢ Q.
 Proof. by intros HP; rewrite -HP right_id. Qed.
 Lemma wand_intro_l P Q R : (Q ∗ P ⊢ R) → P ⊢ Q -∗ R.
 Proof. rewrite comm; apply wand_intro_r. Qed.
@@ -392,14 +392,14 @@ Proof. apply (anti_symm _); auto. apply wand_intro_l; by rewrite right_id. Qed.
 Lemma wand_True P : (True -∗ P) ⊣⊢ P.
 Proof.
   apply (anti_symm _); last by auto using wand_intro_l.
-  eapply sep_elim_True_l; first reflexivity. by rewrite wand_elim_r.
+  eapply sep_elim_True_l; last by apply wand_elim_r. done.
 Qed.
-Lemma wand_entails P Q : (True ⊢ P -∗ Q) → P ⊢ Q.
+Lemma wand_entails P Q : (P -∗ Q)%I → P ⊢ Q.
 Proof.
   intros HPQ. eapply sep_elim_True_r; first exact: HPQ. by rewrite wand_elim_r.
 Qed.
-Lemma entails_wand P Q : (P ⊢ Q) → True ⊢ P -∗ Q.
-Proof. auto using wand_intro_l. Qed.
+Lemma entails_wand P Q : (P ⊢ Q) → (P -∗ Q)%I.
+Proof. intro. apply wand_intro_l. auto. Qed.
 Lemma wand_curry P Q R : (P -∗ Q -∗ R) ⊣⊢ (P ∗ Q -∗ R).
 Proof.
   apply (anti_symm _).
@@ -636,7 +636,7 @@ Proof. by intros; rewrite ownM_valid cmra_valid_elim. Qed.
 Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
 Proof. intros a b [b' ->]. rewrite ownM_op. eauto. Qed.
 Lemma ownM_empty' : uPred_ownM ∅ ⊣⊢ True.
-Proof. apply (anti_symm _); auto using ownM_empty. Qed.
+Proof. apply (anti_symm _); first by auto. apply ownM_empty. Qed.
 Lemma always_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
 Proof.
   intros; apply (anti_symm _); first by apply:always_elim.
@@ -781,4 +781,5 @@ Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed.
 Lemma always_entails_r P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
 Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
 End derived.
+
 End uPred_derived.
diff --git a/base_logic/double_negation.v b/base_logic/double_negation.v
index 52ae21612b3605693fddf51f66caf3250b67a327..ae98efaa8e70c69e6cf566f6ecfa0bdcd7fbcd13 100644
--- a/base_logic/double_negation.v
+++ b/base_logic/double_negation.v
@@ -306,7 +306,7 @@ End classical.
    we establish adequacy without axioms? Unfortunately not, because adequacy for 
    nnupd would imply double negation elimination, which is classical: *)
 
-Lemma nnupd_dne φ: True ⊢ (|=n=> ⌜¬¬ φ → φ⌝: uPred M)%I.
+Lemma nnupd_dne φ: (|=n=> ⌜¬¬ φ → φ⌝: uPred M)%I.
 Proof.
   rewrite /uPred_nnupd. apply forall_intro=>n.
   apply wand_intro_l. rewrite ?right_id. 
@@ -358,7 +358,7 @@ Proof.
     eapply IHn; eauto.
 Qed.
 
-Lemma adequacy φ n : (True ⊢ Nat.iter n (λ P, |=n=> ▷ P) ⌜φ⌝) → ¬¬ φ.
+Lemma adequacy φ n : Nat.iter n (λ P, |=n=> ▷ P)%I ⌜φ⌝%I → ¬¬ φ.
 Proof.
   cut (∀ x, ✓{S n} x → Nat.iter n (λ P, |=n=> ▷ P)%I ⌜φ⌝%I (S n) x → ¬¬φ).
   { intros help H. eapply (help ∅); eauto using ucmra_unit_validN.
diff --git a/base_logic/lib/auth.v b/base_logic/lib/auth.v
index 4c4647a570f7c7cbd50a2c0994262b0abb8d6dce..0adf6f97aa2e83f0f4e901da8c794fcf69f95f32 100644
--- a/base_logic/lib/auth.v
+++ b/base_logic/lib/auth.v
@@ -109,7 +109,7 @@ Section auth.
     iMod (auth_alloc_strong N E t ∅ with "Hφ") as (γ) "[_ ?]"; eauto.
   Qed.
 
-  Lemma auth_empty γ : True ==∗ auth_own γ ∅.
+  Lemma auth_empty γ : (|==> auth_own γ ∅)%I.
   Proof. by rewrite /auth_own -own_empty. Qed.
 
   Lemma auth_acc E γ a :
diff --git a/base_logic/lib/boxes.v b/base_logic/lib/boxes.v
index 1343d4a4e7103fa92ce3a24925e57f6ea7d99a19..5ecb2d037fc3518a1c7c2048341b3730957a38c8 100644
--- a/base_logic/lib/boxes.v
+++ b/base_logic/lib/boxes.v
@@ -70,7 +70,7 @@ Proof.
 Qed.
 
 Lemma box_own_agree γ Q1 Q2 :
-  (box_own_prop γ Q1 ∗ box_own_prop γ Q2) ⊢ ▷ (Q1 ≡ Q2).
+  box_own_prop γ Q1 ∗ box_own_prop γ Q2 ⊢ ▷ (Q1 ≡ Q2).
 Proof.
   rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_r.
   rewrite option_validI /= agree_validI agree_equivI later_equivI /=.
@@ -78,7 +78,7 @@ Proof.
   iRewrite "HQ". by rewrite iProp_fold_unfold.
 Qed.
 
-Lemma box_alloc : True ⊢ box N ∅ True.
+Lemma box_alloc : box N ∅ True%I.
 Proof.
   iIntros; iExists (λ _, True)%I; iSplit.
   - iNext. by rewrite big_sepM_empty.
diff --git a/base_logic/lib/cancelable_invariants.v b/base_logic/lib/cancelable_invariants.v
index a3b196b62f75a30d4cdef4ff299134bb3a618481..0d4e9a3146785da55f1724ec255a487aab792d1b 100644
--- a/base_logic/lib/cancelable_invariants.v
+++ b/base_logic/lib/cancelable_invariants.v
@@ -50,7 +50,7 @@ Section proofs.
     iMod (inv_alloc N _ (P ∨ own γ 1%Qp)%I with "[HP]"); eauto.
   Qed.
 
-  Lemma cinv_cancel E N γ P : ↑N ⊆ E → cinv N γ P ⊢ cinv_own γ 1 ={E}=∗ ▷ P.
+  Lemma cinv_cancel E N γ P : ↑N ⊆ E → cinv N γ P -∗ cinv_own γ 1 ={E}=∗ ▷ P.
   Proof.
     rewrite /cinv. iIntros (?) "#Hinv Hγ".
     iInv N as "[$|>Hγ']" "Hclose"; first iApply "Hclose"; eauto.
@@ -59,7 +59,7 @@ Section proofs.
 
   Lemma cinv_open E N γ p P :
     ↑N ⊆ E →
-    cinv N γ P ⊢ cinv_own γ p ={E,E∖↑N}=∗ ▷ P ∗ cinv_own γ p ∗ (▷ P ={E∖↑N,E}=∗ True).
+    cinv N γ P -∗ cinv_own γ p ={E,E∖↑N}=∗ ▷ P ∗ cinv_own γ p ∗ (▷ P ={E∖↑N,E}=∗ True).
   Proof.
     rewrite /cinv. iIntros (?) "#Hinv Hγ".
     iInv N as "[$|>Hγ']" "Hclose".
diff --git a/base_logic/lib/counter_examples.v b/base_logic/lib/counter_examples.v
index a70bb01e7d697fabf3a1d3f9c7fd289816178758..be5b0b12151831747b41bbdda328c4632f9253e5 100644
--- a/base_logic/lib/counter_examples.v
+++ b/base_logic/lib/counter_examples.v
@@ -13,13 +13,13 @@ Module savedprop. Section savedprop.
   Context (sprop : Type) (saved : sprop → iProp → iProp).
   Hypothesis sprop_persistent : ∀ i P, PersistentP (saved i P).
   Hypothesis sprop_alloc_dep :
-    ∀ (P : sprop → iProp), True ==∗ (∃ i, saved i (P i)).
+    ∀ (P : sprop → iProp), (|==> (∃ i, saved i (P i)))%I.
   Hypothesis sprop_agree : ∀ i P Q, saved i P ∧ saved i Q ⊢ □ (P ↔ Q).
 
   (** A bad recursive reference: "Assertion with name [i] does not hold" *)
   Definition A (i : sprop) : iProp := ∃ P, ¬ P ∗ saved i P.
 
-  Lemma A_alloc : True ==∗ ∃ i, saved i (A i).
+  Lemma A_alloc : (|==> ∃ i, saved i (A i))%I.
   Proof. by apply sprop_alloc_dep. Qed.
 
   Lemma saved_NA i : saved i (A i) ⊢ ¬ A i.
@@ -85,7 +85,7 @@ Module inv. Section inv.
   Context (gname : Type).
   Context (start finished : gname → iProp).
 
-  Hypothesis sts_alloc : True ⊢ fupd M0 (∃ γ, start γ).
+  Hypothesis sts_alloc : fupd M0 (∃ γ, start γ).
   Hypotheses start_finish : ∀ γ, start γ ⊢ fupd M0 (finished γ).
 
   Hypothesis finished_not_start : ∀ γ, start γ ∗ finished γ ⊢ False.
@@ -93,7 +93,7 @@ Module inv. Section inv.
   Hypothesis finished_dup : ∀ γ, finished γ ⊢ finished γ ∗ finished γ.
 
   (** We assume that we cannot update to false. *)
-  Hypothesis consistency : ¬ (True ⊢ fupd M1 False).
+  Hypothesis consistency : ¬ (fupd M1 False).
 
   (** Some general lemmas and proof mode compatibility. *)
   Lemma inv_open' i P R : inv i P ∗ (P -∗ fupd M0 (P ∗ fupd M1 R)) ⊢ fupd M1 R.
@@ -110,7 +110,7 @@ Module inv. Section inv.
     intros P Q; rewrite !uPred.equiv_spec=> -[??]; split; by apply fupd_mono.
   Qed.
 
-  Lemma fupd_frame_r E P Q : (fupd E P ∗ Q) ⊢ fupd E (P ∗ Q).
+  Lemma fupd_frame_r E P Q : fupd E P ∗ Q ⊢ fupd E (P ∗ Q).
   Proof. by rewrite comm fupd_frame_l comm. Qed.
 
   Global Instance elim_fupd_fupd E P Q : ElimModal (fupd E P) P (fupd E Q) (fupd E Q).
@@ -133,7 +133,7 @@ Module inv. Section inv.
     ∃ i, inv i (start γ ∨ (finished γ ∗ □ P)).
   Global Instance saved_persistent γ P : PersistentP (saved γ P) := _.
 
-  Lemma saved_alloc (P : gname → iProp) : True ⊢ fupd M1 (∃ γ, saved γ (P γ)).
+  Lemma saved_alloc (P : gname → iProp) : fupd M1 (∃ γ, saved γ (P γ)).
   Proof.
     iIntros "". iMod (sts_alloc) as (γ) "Hs".
     iMod (inv_alloc (start γ ∨ (finished γ ∗ □ (P γ))) with "[Hs]") as (i) "#Hi".
@@ -166,7 +166,7 @@ Module inv. Section inv.
   Definition A i : iProp := ∃ P, ¬P ∗ saved i P.
   Global Instance A_persistent i : PersistentP (A i) := _.
 
-  Lemma A_alloc : True ⊢ fupd M1 (∃ i, saved i (A i)).
+  Lemma A_alloc : fupd M1 (∃ i, saved i (A i)).
   Proof. by apply saved_alloc. Qed.
 
   Lemma saved_NA i : saved i (A i) ⊢ ¬A i.
diff --git a/base_logic/lib/fancy_updates.v b/base_logic/lib/fancy_updates.v
index 2db972b93352cac1a706246b152681ff2a18009e..5db58a82997ddab8437aec155e90c59fa32c0975 100644
--- a/base_logic/lib/fancy_updates.v
+++ b/base_logic/lib/fancy_updates.v
@@ -22,7 +22,7 @@ Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
 Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)%I
   (at level 99, E1,E2 at level 50, Q at level 200,
    format "P  ={ E1 , E2 }=∗  Q") : uPred_scope.
-Notation "P ={ E1 , E2 }=∗ Q" := (P ⊢ |={E1,E2}=> Q)
+Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)
   (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : C_scope.
 
 Notation "|={ E }=> Q" := (fupd E E Q)
@@ -31,7 +31,7 @@ Notation "|={ E }=> Q" := (fupd E E Q)
 Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)%I
   (at level 99, E at level 50, Q at level 200,
    format "P  ={ E }=∗  Q") : uPred_scope.
-Notation "P ={ E }=∗ Q" := (P ⊢ |={E}=> Q)
+Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)
   (at level 99, E at level 50, Q at level 200, only parsing) : C_scope.
 
 Section fupd.
@@ -56,13 +56,13 @@ Proof. rewrite fupd_eq. iIntros ">H [Hw HE]". iApply "H"; by iFrame. Qed.
 Lemma bupd_fupd E P : (|==> P) ={E}=∗ P.
 Proof. rewrite fupd_eq /fupd_def. by iIntros ">? [$ $] !> !>". Qed.
 
-Lemma fupd_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ={E1,E2}=∗ Q.
+Lemma fupd_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q.
 Proof.
   rewrite fupd_eq /fupd_def. iIntros (HPQ) "HP HwE".
   rewrite -HPQ. by iApply "HP".
 Qed.
 
-Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}=∗ P.
+Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P.
 Proof.
   rewrite fupd_eq /fupd_def. iIntros "HP HwE".
   iMod ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame.
@@ -89,7 +89,7 @@ Proof. intros P Q; apply fupd_mono. Qed.
 
 Lemma fupd_intro E P : P ={E}=∗ P.
 Proof. iIntros "HP". by iApply bupd_fupd. Qed.
-Lemma fupd_intro_mask' E1 E2 : E2 ⊆ E1 → True ⊢ |={E1,E2}=> |={E2,E1}=> True.
+Lemma fupd_intro_mask' E1 E2 : E2 ⊆ E1 → (|={E1,E2}=> |={E2,E1}=> True)%I.
 Proof. exact: fupd_intro_mask. Qed.
 Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=> ◇ P) ={E1,E2}=∗ P.
 Proof. by rewrite {1}(fupd_intro E2 P) except_0_fupd fupd_trans. Qed.
diff --git a/base_logic/lib/own.v b/base_logic/lib/own.v
index 161ec78952eda4be74797330ec7e1a4783876809..7a6ce609afd972421057347923bf8482d6066c00 100644
--- a/base_logic/lib/own.v
+++ b/base_logic/lib/own.v
@@ -68,9 +68,9 @@ Proof.
   (* implicit arguments differ a bit *)
   by trans (✓ cmra_transport inG_prf a : iProp Σ)%I; last destruct inG_prf.
 Qed.
-Lemma own_valid_2 γ a1 a2 : own γ a1 ⊢ own γ a2 -∗ ✓ (a1 ⋅ a2).
+Lemma own_valid_2 γ a1 a2 : own γ a1 -∗ own γ a2 -∗ ✓ (a1 ⋅ a2).
 Proof. apply wand_intro_r. by rewrite -own_op own_valid. Qed.
-Lemma own_valid_3 γ a1 a2 a3 : own γ a1 ⊢ own γ a2 -∗ own γ a3 -∗ ✓ (a1 ⋅ a2 ⋅ a3).
+Lemma own_valid_3 γ a1 a2 a3 : own γ a1 -∗ own γ a2 -∗ own γ a3 -∗ ✓ (a1 ⋅ a2 ⋅ a3).
 Proof. do 2 apply wand_intro_r. by rewrite -!own_op own_valid. Qed.
 Lemma own_valid_r γ a : own γ a ⊢ own γ a ∗ ✓ a.
 Proof. apply (uPred.always_entails_r _ _). apply own_valid. Qed.
@@ -86,20 +86,20 @@ Proof. rewrite !own_eq /own_def; apply _. Qed.
 (* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
    assertion. However, the map_updateP_alloc does not suffice to show this. *)
 Lemma own_alloc_strong a (G : gset gname) :
-  ✓ a → True ==∗ ∃ γ, ⌜γ ∉ G⌝ ∧ own γ a.
+  ✓ a → (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ own γ a)%I.
 Proof.
   intros Ha.
   rewrite -(bupd_mono (∃ m, ⌜∃ γ, γ ∉ G ∧ m = iRes_singleton γ a⌝ ∧ uPred_ownM m)%I).
-  - rewrite ownM_empty.
+  - rewrite /uPred_valid ownM_empty.
     eapply bupd_ownM_updateP, (iprod_singleton_updateP_empty (inG_id _));
       first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
       naive_solver.
   - apply exist_elim=>m; apply pure_elim_l=>-[γ [Hfresh ->]].
     by rewrite !own_eq /own_def -(exist_intro γ) pure_True // left_id.
 Qed.
-Lemma own_alloc a : ✓ a → True ==∗ ∃ γ, own γ a.
+Lemma own_alloc a : ✓ a → (|==> ∃ γ, own γ a)%I.
 Proof.
-  intros Ha. rewrite (own_alloc_strong a ∅) //; [].
+  intros Ha. rewrite /uPred_valid (own_alloc_strong a ∅) //; [].
   apply bupd_mono, exist_mono=>?. eauto with I.
 Qed.
 
@@ -121,10 +121,10 @@ Proof.
   by apply bupd_mono, exist_elim=> a''; apply pure_elim_l=> ->.
 Qed.
 Lemma own_update_2 γ a1 a2 a' :
-  a1 ⋅ a2 ~~> a' → own γ a1 ⊢ own γ a2 ==∗ own γ a'.
+  a1 ⋅ a2 ~~> a' → own γ a1 -∗ own γ a2 ==∗ own γ a'.
 Proof. intros. apply wand_intro_r. rewrite -own_op. by apply own_update. Qed.
 Lemma own_update_3 γ a1 a2 a3 a' :
-  a1 ⋅ a2 ⋅ a3 ~~> a' → own γ a1 ⊢ own γ a2 -∗ own γ a3 ==∗ own γ a'.
+  a1 ⋅ a2 ⋅ a3 ~~> a' → own γ a1 -∗ own γ a2 -∗ own γ a3 ==∗ own γ a'.
 Proof. intros. do 2 apply wand_intro_r. rewrite -!own_op. by apply own_update. Qed.
 End global.
 
@@ -138,9 +138,9 @@ Arguments own_update {_ _} [_] _ _ _ _.
 Arguments own_update_2 {_ _} [_] _ _ _ _ _.
 Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
 
-Lemma own_empty A `{inG Σ (A:ucmraT)} γ : True ==∗ own γ ∅.
+Lemma own_empty A `{inG Σ (A:ucmraT)} γ : (|==> own γ ∅)%I.
 Proof.
-  rewrite ownM_empty !own_eq /own_def.
+  rewrite /uPred_valid ownM_empty !own_eq /own_def.
   apply bupd_ownM_update, iprod_singleton_update_empty.
   apply (alloc_unit_singleton_update (cmra_transport inG_prf ∅)); last done.
   - apply cmra_transport_valid, ucmra_unit_valid.
diff --git a/base_logic/lib/saved_prop.v b/base_logic/lib/saved_prop.v
index a61912f876c630784fe22b4a5db17771db6ad1f4..462a4762d6bb3c4d2ac6c7935fdce400f4b506b0 100644
--- a/base_logic/lib/saved_prop.v
+++ b/base_logic/lib/saved_prop.v
@@ -26,10 +26,10 @@ Section saved_prop.
   Proof. rewrite /saved_prop_own; apply _. Qed.
 
   Lemma saved_prop_alloc_strong x (G : gset gname) :
-    True ==∗ ∃ γ, ⌜γ ∉ G⌝ ∧ saved_prop_own γ x.
+    (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_prop_own γ x)%I.
   Proof. by apply own_alloc_strong. Qed.
 
-  Lemma saved_prop_alloc x : True ==∗ ∃ γ, saved_prop_own γ x.
+  Lemma saved_prop_alloc x : (|==> ∃ γ, saved_prop_own γ x)%I.
   Proof. by apply own_alloc. Qed.
 
   Lemma saved_prop_agree γ x y :
diff --git a/base_logic/lib/thread_local.v b/base_logic/lib/thread_local.v
index 46f2e3204632c886910c03fb6a0ba1bfa3b254d3..021322d7e6f2696434e18c4e3b67ced969f9227b 100644
--- a/base_logic/lib/thread_local.v
+++ b/base_logic/lib/thread_local.v
@@ -37,7 +37,7 @@ Section proofs.
   Global Instance tl_inv_persistent tid N P : PersistentP (tl_inv tid N P).
   Proof. rewrite /tl_inv; apply _. Qed.
 
-  Lemma tl_alloc : True ==∗ ∃ tid, tl_own tid ⊤.
+  Lemma tl_alloc : (|==> ∃ tid, tl_own tid ⊤)%I.
   Proof. by apply own_alloc. Qed.
 
   Lemma tl_own_disjoint tid E1 E2 : tl_own tid E1 ∗ tl_own tid E2 ⊢ ⌜E1 ⊥ E2⌝.
@@ -71,7 +71,7 @@ Section proofs.
 
   Lemma tl_inv_open tid tlE E N P :
     ↑tlN ⊆ tlE → ↑N ⊆ E →
-    tl_inv tid N P ⊢ tl_own tid E ={tlE}=∗ ▷ P ∗ tl_own tid (E∖↑N) ∗
+    tl_inv tid N P -∗ tl_own tid E ={tlE}=∗ ▷ P ∗ tl_own tid (E∖↑N) ∗
                        (▷ P ∗ tl_own tid (E∖↑N) ={tlE}=∗ tl_own tid E).
   Proof.
     rewrite /tl_inv. iIntros (??) "#Htlinv Htoks".
diff --git a/base_logic/lib/viewshifts.v b/base_logic/lib/viewshifts.v
index 02b91ef702c57c96c3e2ce5108825626a2a64c40..151bf0c5047faff6e5077658c3119cb01bcb5956 100644
--- a/base_logic/lib/viewshifts.v
+++ b/base_logic/lib/viewshifts.v
@@ -13,10 +13,10 @@ Notation "P ={ E }=> Q" := (P ={E,E}=> Q)%I
   (at level 99, E at level 50, Q at level 200,
    format "P  ={ E }=>  Q") : uPred_scope.
 
-Notation "P ={ E1 , E2 }=> Q" := (True ⊢ P ={E1,E2}=> Q)%I
+Notation "P ={ E1 , E2 }=> Q" := (P ={E1,E2}=> Q)%I
   (at level 99, E1,E2 at level 50, Q at level 200,
    format "P  ={ E1 , E2 }=>  Q") : C_scope.
-Notation "P ={ E }=> Q" := (True ⊢ P ={E}=> Q)%I
+Notation "P ={ E }=> Q" := (P ={E}=> Q)%I
   (at level 99, E at level 50, Q at level 200,
    format "P  ={ E }=>  Q") : C_scope.
 
diff --git a/base_logic/lib/wsat.v b/base_logic/lib/wsat.v
index b75702333615083123601d5df3705813a176ef9e..4489034ab5ffbb0b9124f20b85826b7390872168 100644
--- a/base_logic/lib/wsat.v
+++ b/base_logic/lib/wsat.v
@@ -52,8 +52,8 @@ Qed.
 Global Instance ownI_persistent i P : PersistentP (ownI i P).
 Proof. rewrite /ownI. apply _. Qed.
 
-Lemma ownE_empty : True ==∗ ownE ∅.
-Proof. by rewrite (own_empty (coPset_disjUR) enabled_name). Qed.
+Lemma ownE_empty : (|==> ownE ∅)%I.
+Proof. by rewrite /uPred_valid (own_empty (coPset_disjUR) enabled_name). Qed.
 Lemma ownE_op E1 E2 : E1 ⊥ E2 → ownE (E1 ∪ E2) ⊣⊢ ownE E1 ∗ ownE E2.
 Proof. intros. by rewrite /ownE -own_op coPset_disj_union. Qed.
 Lemma ownE_disjoint E1 E2 : ownE E1 ∗ ownE E2 ⊢ ⌜E1 ⊥ E2⌝.
@@ -67,8 +67,8 @@ Qed.
 Lemma ownE_singleton_twice i : ownE {[i]} ∗ ownE {[i]} ⊢ False.
 Proof. rewrite ownE_disjoint. iIntros (?); set_solver. Qed.
 
-Lemma ownD_empty : True ==∗ ownD ∅.
-Proof. by rewrite (own_empty (gset_disjUR positive) disabled_name). Qed.
+Lemma ownD_empty : (|==> ownD ∅)%I.
+Proof. by rewrite /uPred_valid (own_empty (gset_disjUR positive) disabled_name). Qed.
 Lemma ownD_op E1 E2 : E1 ⊥ E2 → ownD (E1 ∪ E2) ⊣⊢ ownD E1 ∗ ownD E2.
 Proof. intros. by rewrite /ownD -own_op gset_disj_union. Qed.
 Lemma ownD_disjoint E1 E2 : ownD E1 ∗ ownD E2 ⊢ ⌜E1 ⊥ E2⌝.
diff --git a/base_logic/primitive.v b/base_logic/primitive.v
index b8c73414d6fa4ff258a6d04a30023cf113c2dbfc..27896d8d2c0fb0e6ef70423949eddcca8532ed82 100644
--- a/base_logic/primitive.v
+++ b/base_logic/primitive.v
@@ -188,6 +188,10 @@ Notation "P ==∗ Q" := (P ⊢ |==> Q)
 Notation "P ==∗ Q" := (P -∗ |==> Q)%I
   (at level 99, Q at level 200, format "P  ==∗  Q") : uPred_scope.
 
+Coercion uPred_valid {M} (P : uPred M) : Prop := True%I ⊢ P.
+Notation "P -∗ Q" := (P ⊢ Q)
+  (at level 99, Q at level 200, right associativity, only parsing) : C_scope.
+
 Module uPred_primitive.
 Definition unseal :=
   (uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
@@ -314,6 +318,10 @@ Proof.
     exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l.
 Qed.
 Global Instance bupd_proper : Proper ((≡) ==> (≡)) (@uPred_bupd M) := ne_proper _.
+Global Instance uPred_valid_proper : Proper ((⊣⊢) ==> iff) (@uPred_valid M).
+Proof. solve_proper. Qed.
+Global Instance uPred_valid_mono : Proper ((⊢) ==> impl) (@uPred_valid M).
+Proof. solve_proper. Qed.
 
 (** Introduction and elimination rules *)
 Lemma pure_intro φ P : φ → P ⊢ ⌜φ⌝.
@@ -355,7 +363,7 @@ Proof. unseal; split=> n x ??; by exists a. Qed.
 Lemma exist_elim {A} (Φ : A → uPred M) Q : (∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q.
 Proof. unseal; intros HΦΨ; split=> n x ? [a ?]; by apply HΦΨ with a. Qed.
 
-Lemma internal_eq_refl {A : ofeT} (a : A) : True ⊢ a ≡ a.
+Lemma internal_eq_refl {A : ofeT} (a : A) : uPred_valid (M:=M) (a ≡ a).
 Proof. unseal; by split=> n x ??; simpl. Qed.
 Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → uPred M) P
   {HΨ : ∀ n, Proper (dist n ==> dist n) Ψ} : (P ⊢ a ≡ b) → (P ⊢ Ψ a) → P ⊢ Ψ b.
@@ -491,7 +499,7 @@ Lemma always_ownM_core (a : M) : uPred_ownM a ⊢ □ uPred_ownM (core a).
 Proof.
   split=> n x /=; unseal; intros Hx. simpl. by apply cmra_core_monoN.
 Qed.
-Lemma ownM_empty : True ⊢ uPred_ownM ∅.
+Lemma ownM_empty : uPred_valid (M:=M) (uPred_ownM ∅).
 Proof. unseal; split=> n x ??; by  exists x; rewrite left_id. Qed.
 Lemma later_ownM a : ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ (a ≡ b).
 Proof.
@@ -506,7 +514,7 @@ Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
 Proof.
   unseal; split=> n x Hv [a' ?]; cofe_subst; eauto using cmra_validN_op_l.
 Qed.
-Lemma cmra_valid_intro {A : cmraT} (a : A) : ✓ a → True ⊢ ✓ a.
+Lemma cmra_valid_intro {A : cmraT} (a : A) : ✓ a → uPred_valid (M:=M) (✓ a).
 Proof. unseal=> ?; split=> n x ? _ /=; by apply cmra_valid_validN. Qed.
 Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
 Proof. unseal=> Ha; split=> n x ??; apply Ha, cmra_validN_le with n; auto. Qed.
diff --git a/base_logic/soundness.v b/base_logic/soundness.v
index 4f3c5f793115ddb0bf31ca69173c427259d13752..501d8f1a2f0f106edefa8319acb784e7b96be3eb 100644
--- a/base_logic/soundness.v
+++ b/base_logic/soundness.v
@@ -1,11 +1,11 @@
-From iris.base_logic Require Export primitive.
+From iris.base_logic Require Export primitive derived.
 Import uPred_entails uPred_primitive.
 
 Section adequacy.
 Context {M : ucmraT}.
 
 (** Consistency and adequancy statements *)
-Lemma soundness φ n : (True ⊢ Nat.iter n (λ P, |==> ▷ P) (@uPred_pure M φ)) → φ.
+Lemma soundness φ n : (Nat.iter n (λ P, |==> ▷ P) (@uPred_pure M φ))%I → φ.
 Proof.
   cut (∀ x, ✓{n} x → Nat.iter n (λ P, |==> ▷ P)%I (@uPred_pure M φ) n x → φ).
   { intros help H. eapply (help ∅); eauto using ucmra_unit_validN.
@@ -16,9 +16,9 @@ Proof.
 Qed.
 
 Corollary consistency_modal n :
-  ¬ (True ⊢ Nat.iter n (λ P, |==> ▷ P) (False : uPred M)).
+  ¬ (Nat.iter n (λ P, |==> ▷ P) (False : uPred M))%I.
 Proof. exact (soundness False n). Qed.
 
-Corollary consistency : ¬ (True ⊢ False : uPred M).
+Corollary consistency : ¬ (False : uPred M)%I.
 Proof. exact (consistency_modal 0). Qed.
 End adequacy.
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 3e96e4a1b678512ac256b41f1181217877bff56a..94025c311a3cb5bdc5661a17fbc33fa06b05d4fb 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -189,7 +189,7 @@ Proof.
   - iExists γ, P, R2, i2. iFrame; auto.
 Qed.
 
-Lemma recv_weaken l P1 P2 : (P1 -∗ P2) ⊢ recv l P1 -∗ recv l P2.
+Lemma recv_weaken l P1 P2 : (P1 -∗ P2) -∗ recv l P1 -∗ recv l P2.
 Proof.
   rewrite /recv.
   iIntros "HP HP1"; iDestruct "HP1" as (γ P Q i) "(#Hctx&Hγ&Hi&HP1)".
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index b789b798b695c46d81870e35ba05d638a8ff0b69..1ebdb806436da3f08ac6d773201490acd153b65a 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -38,7 +38,7 @@ Proof. intros [??%subG_inG]%subG_inv; constructor; apply _. Qed.
 
 
 (* Allocation *)
-Lemma wsat_alloc `{invPreG Σ} : True ==∗ ∃ _ : invG Σ, wsat ∗ ownE ⊤.
+Lemma wsat_alloc `{invPreG Σ} : (|==> ∃ _ : invG Σ, wsat ∗ ownE ⊤)%I.
 Proof.
   iIntros.
   iMod (own_alloc (● (∅ : gmap _ _))) as (γI) "HI"; first done.
@@ -50,7 +50,7 @@ Proof.
 Qed.
 
 Lemma iris_alloc `{irisPreG' Λstate Σ} σ :
-  True ==∗ ∃ _ : irisG' Λstate Σ, wsat ∗ ownE ⊤ ∗ ownP_auth σ ∗ ownP σ.
+  (|==> ∃ _ : irisG' Λstate Σ, wsat ∗ ownE ⊤ ∗ ownP_auth σ ∗ ownP σ)%I.
 Proof.
   iIntros.
   iMod wsat_alloc as (?) "[Hws HE]".
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 8c18831da0a8cf313b986ba48daf53ece7838504..f494db58c8c718480f926e0bb6fa1b03012d5447 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -7,29 +7,17 @@ Definition ht `{irisG Λ Σ} (E : coPset) (P : iProp Σ)
   (□ (P -∗ WP e @ E {{ Φ }}))%I.
 Instance: Params (@ht) 4.
 
-Notation "{{ P } } e @ E {{ Φ } }" := (ht E P e%E Φ)
-  (at level 20, P, e, Φ at level 200,
-   format "{{  P  } }  e  @  E  {{  Φ  } }") : uPred_scope.
-Notation "{{ P } } e {{ Φ } }" := (ht ⊤ P e%E Φ)
-  (at level 20, P, e, Φ at level 200,
-   format "{{  P  } }  e  {{  Φ  } }") : uPred_scope.
-Notation "{{ P } } e @ E {{ Φ } }" := (True ⊢ ht E P e%E Φ)
+Notation "{{ P } } e @ E {{ Φ } }" := (ht E P%I e%E Φ%I)
   (at level 20, P, e, Φ at level 200,
    format "{{  P  } }  e  @  E  {{  Φ  } }") : C_scope.
-Notation "{{ P } } e {{ Φ } }" := (True ⊢ ht ⊤ P e%E Φ)
+Notation "{{ P } } e {{ Φ } }" := (ht ⊤ P%I e%E Φ%I)
   (at level 20, P, e, Φ at level 200,
    format "{{  P  } }  e  {{  Φ  } }") : C_scope.
 
-Notation "{{ P } } e @ E {{ v , Q } }" := (ht E P e%E (λ v, Q))
-  (at level 20, P, e, Q at level 200,
-   format "{{  P  } }  e  @  E  {{  v ,  Q  } }") : uPred_scope.
-Notation "{{ P } } e {{ v , Q } }" := (ht ⊤ P e%E (λ v, Q))
-  (at level 20, P, e, Q at level 200,
-   format "{{  P  } }  e  {{  v ,  Q  } }") : uPred_scope.
-Notation "{{ P } } e @ E {{ v , Q } }" := (True ⊢ ht E P e%E (λ v, Q))
+Notation "{{ P } } e @ E {{ v , Q } }" := (ht E P%I e%E (λ v, Q)%I)
   (at level 20, P, e, Q at level 200,
    format "{{  P  } }  e  @  E  {{  v ,  Q  } }") : C_scope.
-Notation "{{ P } } e {{ v , Q } }" := (True ⊢ ht ⊤ P e%E (λ v, Q))
+Notation "{{ P } } e {{ v , Q } }" := (ht ⊤ P%I e%E (λ v, Q)%I)
   (at level 20, P, e, Q at level 200,
    format "{{  P  } }  e  {{  v ,  Q  } }") : C_scope.
 
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index cac72d01bb2e7004d3a3404b853db3ae7efb3aa5..086febe0f4e7380fa66b6d9e61fdcadda981bb75 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -89,20 +89,20 @@ Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
 
 Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _,
-      P ⊢ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }})
+      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }})
     (at level 20, x closed binder, y closed binder,
      format "{{{  P  } } }  e  {{{  x .. y ,  RET  pat ;  Q } } }") : C_scope.
 Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _,
-      P ⊢ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }})
+      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }})
     (at level 20, x closed binder, y closed binder,
      format "{{{  P  } } }  e  @  E  {{{  x .. y ,  RET  pat ;  Q } } }") : C_scope.
 Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
-  (∀ Φ : _ → uPred _, P ⊢ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }})
+  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }})
     (at level 20,
      format "{{{  P  } } }  e  {{{  RET  pat ;  Q } } }") : C_scope.
 Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
-  (∀ Φ : _ → uPred _, P ⊢ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }})
+  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }})
     (at level 20,
      format "{{{  P  } } }  e  @  E  {{{  RET  pat ;  Q } } }") : C_scope.
 
@@ -276,7 +276,7 @@ Lemma wp_frame_step_r' E e Φ R :
 Proof. iIntros (?) "[??]". iApply (wp_frame_step_r E E); try iFrame; eauto. Qed.
 
 Lemma wp_wand E e Φ Ψ :
-  WP e @ E {{ Φ }} ⊢ (∀ v, Φ v -∗ Ψ v) -∗ WP e @ E {{ Ψ }}.
+  WP e @ E {{ Φ }} -∗ (∀ v, Φ v -∗ Ψ v) -∗ WP e @ E {{ Ψ }}.
 Proof.
   iIntros "Hwp H". iApply (wp_strong_mono E); auto.
   iFrame "Hwp". iIntros (?) "?". by iApply "H".
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 5fef411c249465694f2e9e2d160b4feca67ad15e..f741bd26be26d33d4d1facacb3ba151828262889 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -358,7 +358,7 @@ Global Instance Envs_mono (R : relation (uPred M)) :
 Proof. by constructor. Qed.
 
 (** * Adequacy *)
-Lemma tac_adequate P : (Envs Enil Enil ⊢ P) → True ⊢ P.
+Lemma tac_adequate P : (Envs Enil Enil ⊢ P) → P.
 Proof.
   intros <-. rewrite /of_envs /= always_pure !right_id.
   apply pure_intro; repeat constructor.
@@ -618,7 +618,7 @@ Proof.
 Qed.
 
 Lemma tac_pose_proof Δ Δ' j P Q :
-  (True ⊢ P) →
+  P →
   envs_app true (Esnoc Enil j P) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 331ec21ebaa4d0cd88cd356141c466e3f5b160d7..603e332535916ea9a8fafabf80786178df8ed54e 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -47,6 +47,7 @@ Tactic Notation "iProof" :=
   | |- of_envs _ ⊢ _ => fail "iProof: already in Iris proofmode"
   | |- ?P =>
     match eval hnf in P with
+    (* need to use the unfolded version of [uPred_valid] due to the hnf *)
     | True ⊢ _ => apply tac_adequate
     | _ ⊢ _ => apply uPred.wand_entails, tac_adequate
     (* need to use the unfolded version of [⊣⊢] due to the hnf *)
@@ -355,16 +356,16 @@ Tactic Notation "iSpecialize" open_constr(t) "#" :=
   iSpecializeCore t as true (fun _ => idtac).
 
 (** * Pose proof *)
-(* The tactic [iIntoEntails] tactic solves a goal [True ⊢ Q]. The arguments [t]
-is a Coq term whose type is of the following shape:
+(* The tactic [iIntoValid] tactic solves a goal [uPred_valid Q]. The
+arguments [t] is a Coq term whose type is of the following shape:
 
-- [∀ (x_1 : A_1) .. (x_n : A_n), True ⊢ Q]
+- [∀ (x_1 : A_1) .. (x_n : A_n), uPred_valid Q]
 - [∀ (x_1 : A_1) .. (x_n : A_n), P1 ⊢ P2], in which case [Q] becomes [P1 -∗ P2]
 - [∀ (x_1 : A_1) .. (x_n : A_n), P1 ⊣⊢ P2], in which case [Q] becomes [P1 ↔ P2]
 
 The tactic instantiates each dependent argument [x_i] with an evar and generates
 a goal [P] for non-dependent arguments [x_i : P]. *)
-Tactic Notation "iIntoEntails" open_constr(t) :=
+Tactic Notation "iIntoValid" open_constr(t) :=
   let rec go t :=
     let tT := type of t in
     lazymatch eval hnf in tT with
@@ -392,7 +393,7 @@ Tactic Notation "iPoseProofCore" open_constr(lem) "as" constr(p) tactic(tac) :=
          |tac Htmp]
     | _ =>
        eapply tac_pose_proof with _ Htmp _; (* (j:=H) *)
-         [iIntoEntails t
+         [iIntoValid t
          |env_cbv; reflexivity || fail "iPoseProof:" Htmp "not fresh"
          |tac Htmp]
     end;
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index bff108e15ae07909fdb2f4a1e8899e85ee336e81..1ba0ee98bf1d45f839cf552dfd0f766980fec9c8 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -59,7 +59,7 @@ Section LiftingTests.
   Qed.
 
   Lemma Pred_user E :
-    True ⊢ WP let: "x" := Pred #42 in Pred "x" @ E {{ v, ⌜v = #40⌝ }}.
+    (WP let: "x" := Pred #42 in Pred "x" @ E {{ v, ⌜v = #40⌝ }})%I.
   Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed.
 End LiftingTests.
 
diff --git a/tests/proofmode.v b/tests/proofmode.v
index c5de431e0ab1cd9693f422d67af40f4c03c35ab5..df03e0f98087dafdf1f5008dbbb0188f1e85a676 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -12,13 +12,13 @@ Proof.
 Qed.
 
 Lemma demo_1 (M : ucmraT) (P1 P2 P3 : nat → uPred M) :
-  True ⊢ ∀ (x y : nat) a b,
+  (∀ (x y : nat) a b,
     x ≡ y →
     □ (uPred_ownM (a ⋅ b) -∗
     (∃ y1 y2 c, P1 ((x + y1) + y2) ∧ True ∧ □ uPred_ownM c) -∗
     □ ▷ (∀ z, P2 z ∨ True → P2 z) -∗
     ▷ (∀ n m : nat, P1 n → □ ((True ∧ P2 n) → □ (⌜n = n⌝ ↔ P3 n))) -∗
-    ▷ ⌜x = 0⌝ ∨ ∃ x z, ▷ P3 (x + z) ∗ uPred_ownM b ∗ uPred_ownM (core b)).
+    ▷ ⌜x = 0⌝ ∨ ∃ x z, ▷ P3 (x + z) ∗ uPred_ownM b ∗ uPred_ownM (core b)))%I.
 Proof.
   iIntros (i [|j] a b ?) "!# [Ha Hb] H1 #H2 H3"; setoid_subst.
   { iLeft. by iNext. }