diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index ef26c1a7745f5dea760d2393ab70a5d2dc389542..835c77941b44ac5504820f9f0fa821711bbaafeb 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -278,6 +278,13 @@ Proof.
     + by rewrite lookup_op lookup_singleton lookup_partial_alter Hi.
     + by rewrite lookup_op lookup_singleton_ne// lookup_partial_alter_ne// left_id.
 Qed.
+Lemma singleton_included_exclusive m i x :
+  Exclusive x → ✓ m →
+  {[ i := x ]} ≼ m ↔ m !! i ≡ Some x.
+Proof.
+  intros ? Hm. rewrite singleton_included. split; last by eauto.
+  intros (y&?&->%(Some_included_exclusive _)); eauto using lookup_valid_Some.
+Qed.
 
 Global Instance singleton_cancelable i x :
   Cancelable (Some x) → Cancelable {[ i := x ]}.
diff --git a/theories/heap_lang/proph_map.v b/theories/heap_lang/proph_map.v
index 21d9858d3f72adfcdb3649fde23bf60a3864dfdd..cb03d7717069ca17ad0b50754170e979ff17acb5 100644
--- a/theories/heap_lang/proph_map.v
+++ b/theories/heap_lang/proph_map.v
@@ -121,10 +121,8 @@ Section to_proph_map.
   Lemma proph_map_singleton_included R p v :
     {[p := Excl v]} ≼ to_proph_map R → R !! p = Some v.
   Proof.
-    rewrite singleton_included=> -[v' []].
-    rewrite /to_proph_map lookup_fmap fmap_Some_equiv=> -[v'' [Hp ->]].
-    intros [=->]%Some_included_exclusive%leibniz_equiv_iff; first done; last done.
-    apply excl_exclusive.
+    rewrite singleton_included_exclusive; last by apply to_proph_map_valid.
+    by rewrite leibniz_equiv_iff /to_proph_map lookup_fmap fmap_Some=> -[v' [-> [->]]].
   Qed.
 End to_proph_map.