Commonly used variant of `singleton_included` when the element is exclusive.

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 ]}.

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.