diff --git a/tests/proofmode.v b/tests/proofmode.v
index 8a02f7c9f8ffad952003bec104b5632577653bb8..288c75c678a7cb696c4835bbf9dca4ac9842d957 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -43,4 +43,4 @@ Qed.
 
 Lemma demo_3 (M : cmraT) (P1 P2 P3 : uPred M) :
   (P1 ★ P2 ★ P3) ⊢ (▷ P1 ★ ▷ (P2 ★ ∃ x, (P3 ∧ x = 0) ∨ P3)).
-Proof. iIntros "($ & $ & H)". iFrame "H". simpl. iNext. by iExists 0. Qed.
\ No newline at end of file
+Proof. iIntros "($ & $ & H)". iFrame "H". iNext. by iExists 0. Qed.
\ No newline at end of file