diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 84f4d999de9809d819bf4477f35d4c6647fdc749..61762f93c58b6ebab0a6cf230ce67846ac6714e7 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1247,7 +1247,7 @@ Tactic Notation "iAssertCore" open_constr(Q)
        |tac H]
   | [SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs)] =>
      let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
-     match p with
+     match eval cbv in (p && negb m) with
      | false =>
        eapply tac_assert with _ _ _ lr Hs' H Q _;
          [match m with
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 459e3198d0c9f6228b709a77ba4734194ea28af0..8a884b3d74d686e21b503425841a07b413ddb98c 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -124,3 +124,6 @@ Proof. iIntros "H HP HQ". by iApply ("H" with "[HP]"). Qed.
 (* Check coercions *)
 Lemma demo_12 (M : ucmraT) (P : Z → uPred M) : (∀ x, P x) -∗ ∃ x, P x.
 Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed.
+
+Lemma demo_13 (M : ucmraT) (P : uPred M) : (|==> False) -∗ |==> P.
+Proof. iIntros. iAssert False%I with ">[-]" as "[]". done. Qed.