diff --git a/iris_heap_lang/proph_erasure.v b/iris_heap_lang/proph_erasure.v
index 704a56c576dd7746c8795983f8ab400bba6065eb..985c612ce402fe7ae747faf004b27a5805a8c700 100644
--- a/iris_heap_lang/proph_erasure.v
+++ b/iris_heap_lang/proph_erasure.v
@@ -802,7 +802,7 @@ Proof.
   apply nsteps_inv_r in Hstps as [[t3 σ3] [Hstps Hρ]]; simpl in *.
   destruct (IHn _ _ Hstps) as (t2'&t2''&σ2'&Hostps&?&?&Hprstps); simplify_eq.
   edestruct @erased_step_pure_step_tp as [[? Hint]|Hext]; simplify_eq/=;
-    eauto 10; [|done..].
+    first apply Hρ; eauto 10; [].
   destruct Hext as (i&ei&t2'&efs&e'&κ&Hi1&Ht2&Hpstp);
     simplify_eq/=.
   rewrite /erase_tp list_lookup_fmap in Hi1.