diff --git a/theories/logatom/herlihy_wing_queue/hwq.v b/theories/logatom/herlihy_wing_queue/hwq.v
index 428c7b4a6cc611dba3237c85746e28f30c8598ed..91f122b8ba7ab897a74ce795e8e26a9bc0854d46 100644
--- a/theories/logatom/herlihy_wing_queue/hwq.v
+++ b/theories/logatom/herlihy_wing_queue/hwq.v
@@ -2700,7 +2700,6 @@ Proof.
     - iDestruct (contra_agree with "Hinit_cont Hcont") as %[-> ->].
       iPureIntro. split; first done. destruct Hcont as (((H1 & H2) & H3) & _). done.
     - by iDestruct (contra_not_no_contra with "Hcont Hinit_cont") as "False". }
-  SearchAbout "snap".
   (* We resolve. *)
   iDestruct "Hproph" as (rs) "[Hp Hpvs]". iDestruct "Hpvs" as %Hpvs.
   wp_apply (wp_resolve with "Hp"); first done.