diff --git a/theories/heap_lang/proph_map.v b/theories/heap_lang/proph_map.v
index 5f19f0c774c5d75678af3b1d1c42f8ae4ba4d048..8e2a8cd0db8b310de86cc1c51131efb2fb9451ad 100644
--- a/theories/heap_lang/proph_map.v
+++ b/theories/heap_lang/proph_map.v
@@ -72,9 +72,10 @@ Section first_resolve.
     first_resolve_in_list (<[p := first_resolve pvs p]> R) pvs.
   Proof.
     intros Hf Hnotin p' v' Hp'. rewrite (dom_insert_L R p) in Hp'.
-    erewrite elem_of_union in Hp'. destruct Hp' as [->%elem_of_singleton | Hin] => [->].
-    - by rewrite lookup_insert.
-    - rewrite lookup_insert_ne; first auto. by intros ->.
+    erewrite elem_of_union in Hp'. destruct Hp' as [->%elem_of_singleton | Hin].
+    - intros ->. by rewrite lookup_insert.
+    - intros <-%Hf; last done. rewrite lookup_insert_ne; first done.
+      intros ?. subst. done.
   Qed.
 
   Lemma first_resolve_delete pvs p v R :