diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index ed27be14a826d549d31fc2999e2fc3e909991f50..119306c5502037bedebff74f68425b902d80bafa 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -768,3 +768,4 @@ Tactic Notation "iRewrite" "-" open_constr(t) "in" constr(H) :=
 (* Make sure that by and done solve trivial things in proof mode *)
 Hint Extern 0 (of_envs _ ⊢ _) => by iPureIntro.
 Hint Extern 0 (of_envs _ ⊢ _) => iAssumption.
+Hint Resolve uPred.eq_refl'. (* Maybe make an [iReflexivity] tactic *)
diff --git a/tests/proofmode.v b/tests/proofmode.v
index e82db494ee5000c2f4192d9e1c491a6a51869374..d0d7d4eecb175976e45f9834cbd8815868ba57d0 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -67,9 +67,9 @@ Lemma demo_5 (M : ucmraT) (x y : M) (P : uPred M) :
   (∀ z, P → z ≡ y) ⊢ (P -★ (x,x) ≡ (y,x)).
 Proof.
   iIntros "H1 H2".
-  iRewrite (uPred.eq_sym x x with "[#]"). iApply uPred.eq_refl.
+  iRewrite (uPred.eq_sym x x with "[#]"); first done.
   iRewrite -("H1" $! _ with "[#]"); first done.
-  iApply uPred.eq_refl.
+  done.
 Qed.
 
 Lemma demo_6 (M : ucmraT) (P Q : uPred M) :