diff --git a/theories/tests/proofmode_tests.v b/theories/tests/proofmode_tests.v
index 1adc17e8e1d5e3278c26ec082f37cbecbd2a101a..04bfb1015bd3463c134e480eba521c47a34eab70 100644
--- a/theories/tests/proofmode_tests.v
+++ b/theories/tests/proofmode_tests.v
@@ -13,8 +13,6 @@ Lemma test1 A P t :
   REL (#2 + #2) << (λ: <>, t) #() : A.
 Proof.
   iIntros "HP Ht".
-  rel_bind_l #2. Undo.
-  rel_pure_l (_ + _)%E. Undo.
   rel_pure_l. repeat rel_pure_r.
   by iApply "Ht".
 Qed.