diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index c73634130e297a9ba7532c60baa2f8d58a3bf4df..cadd0c88d42f1754a537136758a73a681f743336 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -51,7 +51,7 @@ Proof.
 Qed.
 
 Lemma inv_alloc_open N E P :
-  ↑N ⊆ E → True ={E, E∖↑N}=∗ inv N P ∗ (▷P ={E∖↑N, E}=∗ True).
+  ↑N ⊆ E → (|={E, E∖↑N}=> inv N P ∗ (▷P ={E∖↑N, E}=∗ True))%I.
 Proof.
   rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros (Sub) "[Hw HE]".
   iMod (ownI_alloc_open (∈ (↑N : coPset)) P with "Hw")
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index c3e4052d45c0374a65c6f61d0b75e39b2eecde98..08ed253eb83de83e70011c74c3af6048d98d0fc4 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -190,6 +190,8 @@ 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.
+Typeclasses Opaque uPred_valid.
+
 Notation "P -∗ Q" := (P ⊢ Q)
   (at level 99, Q at level 200, right associativity) : C_scope.
 
diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index 9a4a1115bb788463937d2e65bf991736fdc44549..fa3bc513f177ede6d839a3f2efce31bf0dd20117 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -15,7 +15,7 @@ Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
 Proof. solve_inG. Qed.
 
 Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
-  (∀ `{heapG Σ}, True ⊢ WP e {{ v, ⌜φ v⌝ }}) →
+  (∀ `{heapG Σ}, WP e {{ v, ⌜φ v⌝ }}%I) →
   adequate e σ φ.
 Proof.
   intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
diff --git a/theories/heap_lang/lib/barrier/proof.v b/theories/heap_lang/lib/barrier/proof.v
index 4b51254982f5c837112fc41674b780faad7ca139..fd97bb305259a27065903f24bad88208a7b6342a 100644
--- a/theories/heap_lang/lib/barrier/proof.v
+++ b/theories/heap_lang/lib/barrier/proof.v
@@ -91,7 +91,7 @@ Qed.
 Lemma newbarrier_spec (P : iProp Σ) :
   {{{ True }}} newbarrier #() {{{ l, RET #l; recv l P ∗ send l P }}}.
 Proof.
-  iIntros (Φ) "HΦ".
+  iIntros (Φ) "_ HΦ".
   rewrite -wp_fupd /newbarrier /=. wp_seq. wp_alloc l as "Hl".
   iApply ("HΦ" with "[> -]").
   iMod (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index a4421e1eb38145a4b5a434f2f4b8d236ed432987..297e55c80d04fb226ac4a8cc70136e54c309c0ad 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -35,7 +35,7 @@ Section mono_proof.
   Lemma newcounter_mono_spec (R : iProp Σ) :
     {{{ True }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
   Proof.
-    iIntros (Φ) "HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
+    iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
     iMod (own_alloc (● (O:mnat) ⋅ ◯ (O:mnat))) as (γ) "[Hγ Hγ']"; first done.
     iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
     { iNext. iExists 0%nat. by iFrame. }
@@ -111,7 +111,7 @@ Section contrib_spec.
     {{{ True }}} newcounter #()
     {{{ γ l, RET #l; ccounter_ctx γ l ∗ ccounter γ 1 0 }}}.
   Proof.
-    iIntros (Φ) "HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
+    iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
     iMod (own_alloc (●! O%nat ⋅ ◯! 0%nat)) as (γ) "[Hγ Hγ']"; first done.
     iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
     { iNext. iExists 0%nat. by iFrame. }
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 7368ecf3d581934b9e659bad700133de90a4aae0..e4fb5be3db759f75c2252c2ad2846152d941a97a 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -166,7 +166,7 @@ Lemma wp_alloc E e v :
   to_val e = Some v →
   {{{ True }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
 Proof.
-  iIntros (<-%of_to_val Φ) "HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (<-%of_to_val Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>"; iSplit; first by auto.
   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 0618e26c5b0ff6ffafacc54b255712b578bee5cf..9678b0e9a4a78c92412f11f180e20ecc08fce07c 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -164,9 +164,9 @@ End adequacy.
 
 Theorem wp_adequacy Σ Λ `{invPreG Σ} e σ φ :
   (∀ `{Hinv : invG Σ},
-     True ={⊤}=∗ ∃ stateI : state Λ → iProp Σ,
+     (|={⊤}=> ∃ stateI : state Λ → iProp Σ,
        let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
-       stateI σ ∗ WP e {{ v, ⌜φ v⌝ }}) →
+       stateI σ ∗ WP e {{ v, ⌜φ v⌝ }})%I) →
   adequate e σ φ.
 Proof.
   intros Hwp; split.
@@ -188,9 +188,9 @@ Qed.
 
 Theorem wp_invariance Σ Λ `{invPreG Σ} e σ1 t2 σ2 φ :
   (∀ `{Hinv : invG Σ},
-     True ={⊤}=∗ ∃ stateI : state Λ → iProp Σ,
+     (|={⊤}=> ∃ stateI : state Λ → iProp Σ,
        let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
-       stateI σ1 ∗ WP e {{ _, True }} ∗ (stateI σ2 ={⊤,∅}=∗ ⌜φ⌝)) →
+       stateI σ1 ∗ WP e {{ _, True }} ∗ (stateI σ2 ={⊤,∅}=∗ ⌜φ⌝))%I) →
   rtc step ([e], σ1) (t2, σ2) →
   φ.
 Proof.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 7bc3426de86dd5ee96378c7c4f050f28ddb25ce1..d25a56c5c805854643b6fefdc2a1fa1022831153 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -50,19 +50,25 @@ Tactic Notation "iMatchHyp" tactic1(tac) :=
   | |- context[ environments.Esnoc _ ?x ?P ] => tac x P
   end.
 
+Class AsValid {M} (φ : Prop) (P : uPred M) := as_entails : φ ↔ P.
+Arguments AsValid {_} _%type _%I.
+
+Instance as_valid_valid {M} (P : uPred M) : AsValid (uPred_valid P) P | 0.
+Proof. by rewrite /AsValid. Qed.
+
+Instance as_valid_entails {M} (P Q : uPred M) : AsValid (P ⊢ Q) (P -∗ Q) | 1.
+Proof. split. apply uPred.entails_wand. apply uPred.wand_entails. Qed.
+
+Instance as_valid_equiv {M} (P Q : uPred M) : AsValid (P ≡ Q) (P ↔ Q).
+Proof. split. apply uPred.equiv_iff. apply uPred.iff_equiv. Qed.
+
 (** * Start a proof *)
 Ltac iStartProof :=
   lazymatch goal with
   | |- of_envs _ ⊢ _ => idtac
   | |- ?P =>
-    lazymatch 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 *)
-    | uPred_equiv' _ _ => apply uPred.iff_equiv, tac_adequate
-    | _ => fail "iStartProof: not a uPred"
-    end
+    apply (proj2 (_ : AsValid P _)), tac_adequate
+    || fail "iStartProof: not a uPred"
   end.
 
 (** * Context manipulation *)
@@ -529,18 +535,16 @@ a goal [P] for non-dependent arguments [x_i : P]. *)
 Tactic Notation "iIntoValid" open_constr(t) :=
   let rec go t :=
     let tT := type of t in
-    lazymatch eval hnf in tT with
-    | True ⊢ _ => apply t
-    | _ ⊢ _ => apply (uPred.entails_wand _ _ t)
-    (* need to use the unfolded version of [⊣⊢] due to the hnf *)
-    | uPred_equiv' _ _ => apply (uPred.equiv_iff _ _ t)
-    | ?P → ?Q => let H := fresh in assert P as H; [|go uconstr:(t H); clear H]
-    | ∀ _ : ?T, _ =>
-       (* Put [T] inside an [id] to avoid TC inference from being invoked. *)
-       (* This is a workarround for Coq bug #4969. *)
-       let e := fresh in evar (e:id T);
-       let e' := eval unfold e in e in clear e; go (t e')
-    end in
+    first
+      [apply (proj1 (_ : AsValid tT _) t)
+      |lazymatch eval hnf in tT with
+       | ?P → ?Q => let H := fresh in assert P as H; [|go uconstr:(t H); clear H]
+       | ∀ _ : ?T, _ =>
+         (* Put [T] inside an [id] to avoid TC inference from being invoked. *)
+         (* This is a workarround for Coq bug #4969. *)
+         let e := fresh in evar (e:id T);
+         let e' := eval unfold e in e in clear e; go (t e')
+       end] in
   go t.
 
 (* The tactic [tac] is called with a temporary fresh name [H]. The argument
diff --git a/theories/tests/barrier_client.v b/theories/tests/barrier_client.v
index 0352e068f758ed7e7406cd4011e27bd5f177d099..9703b23746b46053e881855c4bb475be4bbd4aee 100644
--- a/theories/tests/barrier_client.v
+++ b/theories/tests/barrier_client.v
@@ -40,7 +40,7 @@ Section client.
   Lemma client_safe : WP client {{ _, True }}%I.
   Proof.
     iIntros ""; rewrite /client. wp_alloc y as "Hy". wp_let.
-    wp_apply (newbarrier_spec N (y_inv 1 y)).
+    wp_apply (newbarrier_spec N (y_inv 1 y) with "[//]").
     iIntros (l) "[Hr Hs]". wp_let.
     iApply (wp_par (λ _, True%I) (λ _, True%I) with "[Hy Hs] [Hr]"); last auto.
     - (* The original thread, the sender. *)