diff --git a/_CoqProject b/_CoqProject
index 9922e223468d41826a139175cc9c6b74b0e6c7ab..c9539aac94b683d88c9bc53c789428ac4a2cc234 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -67,6 +67,7 @@ theories/base_logic/lib/na_invariants.v
 theories/base_logic/lib/cancelable_invariants.v
 theories/base_logic/lib/gen_heap.v
 theories/base_logic/lib/fancy_updates_from_vs.v
+theories/base_logic/lib/proph_map.v
 theories/program_logic/adequacy.v
 theories/program_logic/lifting.v
 theories/program_logic/weakestpre.v
@@ -89,7 +90,6 @@ theories/heap_lang/notation.v
 theories/heap_lang/proofmode.v
 theories/heap_lang/adequacy.v
 theories/heap_lang/total_adequacy.v
-theories/heap_lang/proph_map.v
 theories/heap_lang/lib/spawn.v
 theories/heap_lang/lib/par.v
 theories/heap_lang/lib/assert.v
diff --git a/theories/base_logic/lib/proph_map.v b/theories/base_logic/lib/proph_map.v
new file mode 100644
index 0000000000000000000000000000000000000000..22f3594928b9b422716a230f13b1ea6ae4f2c878
--- /dev/null
+++ b/theories/base_logic/lib/proph_map.v
@@ -0,0 +1,175 @@
+From iris.algebra Require Import auth list gmap.
+From iris.base_logic.lib Require Export own.
+From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
+Import uPred.
+
+Local Notation proph_map P V := (gmap P (list V)).
+Definition proph_val_list (P V : Type) := list (P * V).
+
+Definition proph_mapUR (P V : Type) `{Countable P} : ucmraT :=
+  gmapUR P $ exclR $ listC $ leibnizC V.
+
+Definition to_proph_map {P V} `{Countable P} (pvs : proph_map P V) : proph_mapUR P V :=
+  fmap (λ vs, Excl (vs : list (leibnizC V))) pvs.
+
+(** The CMRA we need. *)
+Class proph_mapG (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapG {
+  proph_map_inG :> inG Σ (authR (proph_mapUR P V));
+  proph_map_name : gname
+}.
+Arguments proph_map_name {_ _ _ _ _} _ : assert.
+
+Class proph_mapPreG (P V : Type) (Σ : gFunctors) `{Countable P} :=
+  { proph_map_preG_inG :> inG Σ (authR (proph_mapUR P V)) }.
+
+Definition proph_mapΣ (P V : Type) `{Countable P} : gFunctors :=
+  #[GFunctor (authR (proph_mapUR P V))].
+
+Instance subG_proph_mapPreG {Σ P V} `{Countable P} :
+  subG (proph_mapΣ P V) Σ → proph_mapPreG P V Σ.
+Proof. solve_inG. Qed.
+
+Section definitions.
+  Context `{pG : proph_mapG P V Σ}.
+  Implicit Types pvs : proph_val_list P V.
+  Implicit Types R : proph_map P V.
+  Implicit Types p : P.
+
+  (** The list of resolves for [p] in [pvs]. *)
+  Fixpoint proph_list_resolves pvs p : list V :=
+    match pvs with
+    | []         => []
+    | (q,v)::pvs => if decide (p = q) then v :: proph_list_resolves pvs p
+                    else proph_list_resolves pvs p
+    end.
+
+  Definition proph_resolves_in_list R pvs :=
+    map_Forall (λ p vs, vs = proph_list_resolves pvs p) R.
+
+  Definition proph_map_ctx pvs (ps : gset P) : iProp Σ :=
+    (∃ R, ⌜proph_resolves_in_list R pvs ∧
+          dom (gset _) R ⊆ ps⌝ ∗
+          own (proph_map_name pG) (● (to_proph_map R)))%I.
+
+  Definition proph_def (p : P) (vs : list V) : iProp Σ :=
+    own (proph_map_name pG) (â—¯ {[p := Excl vs]}).
+
+  Definition proph_aux : seal (@proph_def). by eexists. Qed.
+  Definition proph := proph_aux.(unseal).
+  Definition proph_eq : @proph = @proph_def := proph_aux.(seal_eq).
+End definitions.
+
+Section list_resolves.
+  Context {P V : Type} `{Countable P}.
+  Implicit Type pvs : proph_val_list P V.
+  Implicit Type p : P.
+  Implicit Type R : proph_map P V.
+
+  Lemma resolves_insert pvs p R :
+    proph_resolves_in_list R pvs →
+    p ∉ dom (gset _) R →
+    proph_resolves_in_list (<[p := proph_list_resolves pvs p]> R) pvs.
+  Proof.
+    intros Hinlist Hp q vs HEq.
+    destruct (decide (p = q)) as [->|NEq].
+    - rewrite lookup_insert in HEq. by inversion HEq.
+    - rewrite lookup_insert_ne in HEq; last done. by apply Hinlist.
+  Qed.
+End list_resolves.
+
+Section to_proph_map.
+  Context (P V : Type) `{Countable P}.
+  Implicit Types p : P.
+  Implicit Types vs : list V.
+  Implicit Types R : proph_map P V.
+
+  Lemma to_proph_map_valid R : ✓ to_proph_map R.
+  Proof. intros l. rewrite lookup_fmap. by case (R !! l). Qed.
+
+  Lemma to_proph_map_insert p vs R :
+    to_proph_map (<[p := vs]> R) = <[p := Excl (vs: list (leibnizC V))]> (to_proph_map R).
+  Proof. by rewrite /to_proph_map fmap_insert. Qed.
+
+  Lemma to_proph_map_delete p R :
+    to_proph_map (delete p R) = delete p (to_proph_map R).
+  Proof. by rewrite /to_proph_map fmap_delete. Qed.
+
+  Lemma lookup_to_proph_map_None R p :
+    R !! p = None → to_proph_map R !! p = None.
+  Proof. by rewrite /to_proph_map lookup_fmap=> ->. Qed.
+
+  Lemma proph_map_singleton_included R p vs :
+    {[p := Excl vs]} ≼ to_proph_map R → R !! p = Some vs.
+  Proof.
+    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.
+
+Lemma proph_map_init `{Countable P, !proph_mapPreG P V PVS} pvs ps :
+  (|==> ∃ _ : proph_mapG P V PVS, proph_map_ctx pvs ps)%I.
+Proof.
+  iMod (own_alloc (● to_proph_map ∅)) as (γ) "Hh".
+  { apply: auth_auth_valid. exact: to_proph_map_valid. }
+  iModIntro. iExists (ProphMapG P V PVS _ _ _ γ), ∅. iSplit; last by iFrame.
+  iPureIntro. split =>//.
+Qed.
+
+Section proph_map.
+  Context `{proph_mapG P V Σ}.
+  Implicit Types p : P.
+  Implicit Types v : V.
+  Implicit Types vs : list V.
+  Implicit Types R : proph_map P V.
+  Implicit Types ps : gset P.
+
+  (** General properties of mapsto *)
+  Global Instance proph_timeless p vs : Timeless (proph p vs).
+  Proof. rewrite proph_eq /proph_def. apply _. Qed.
+
+  Lemma proph_map_new_proph p ps pvs :
+    p ∉ ps →
+    proph_map_ctx pvs ps ==∗
+    proph_map_ctx pvs ({[p]} ∪ ps) ∗ proph p (proph_list_resolves pvs p).
+  Proof.
+    iIntros (Hp) "HR". iDestruct "HR" as (R) "[[% %] H●]".
+    rewrite proph_eq /proph_def.
+    iMod (own_update with "H●") as "[H● H◯]".
+    { eapply auth_update_alloc, (alloc_singleton_local_update _ p (Excl _))=> //.
+      apply lookup_to_proph_map_None.
+      apply (not_elem_of_dom (D:=gset P)). set_solver. }
+    iModIntro. iFrame.
+    iExists (<[p := proph_list_resolves pvs p]> R). iSplitR "H●".
+    - iPureIntro. split.
+      + apply resolves_insert; first done. set_solver.
+      + rewrite dom_insert. set_solver.
+    - by rewrite /to_proph_map fmap_insert.
+  Qed.
+
+  Lemma proph_map_resolve_proph p v pvs ps vs :
+    proph_map_ctx ((p,v) :: pvs) ps ∗ proph p vs ==∗
+    ∃vs', ⌜vs = v::vs'⌝ ∗ proph_map_ctx pvs ps ∗ proph p vs'.
+  Proof.
+    iIntros "[HR Hp]". iDestruct "HR" as (R) "[HP H●]". iDestruct "HP" as %[Hres Hdom].
+    rewrite /proph_map_ctx proph_eq /proph_def.
+    iDestruct (own_valid_2 with "H● Hp") as %[HR%proph_map_singleton_included _]%auth_valid_discrete_2.
+    assert (vs = v :: proph_list_resolves pvs p) as ->.
+    { rewrite (Hres p vs HR). simpl. by rewrite decide_True. }
+    iMod (own_update_2 with "H● Hp") as "[H● H◯]".
+    { eapply auth_update. apply: singleton_local_update.
+      - by rewrite /to_proph_map lookup_fmap HR.
+      - by apply (exclusive_local_update _ (Excl (proph_list_resolves pvs p : list (leibnizC V)))). }
+    rewrite /to_proph_map -fmap_insert.
+    iModIntro. iExists (proph_list_resolves pvs p). iFrame. iSplitR.
+    - iPureIntro. done.
+    - iExists _. iFrame. iPureIntro. split.
+      + intros q ws HEq. destruct (decide (p = q)) as [<-|NEq].
+        * rewrite lookup_insert in HEq. by inversion HEq.
+        * rewrite lookup_insert_ne in HEq; last done.
+          rewrite (Hres q ws HEq).
+          simpl. rewrite decide_False; done.
+      + assert (p ∈ dom (gset P) R) by exact: elem_of_dom_2.
+        rewrite dom_insert. set_solver.
+  Qed.
+End proph_map.
diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index 4bfe13696527a5e87670f013ab3c82653688398b..217ca2cae9d0de204601aedcc1edef8ecaf78544 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -1,6 +1,7 @@
 From iris.program_logic Require Export weakestpre adequacy.
 From iris.algebra Require Import auth.
-From iris.heap_lang Require Import proofmode notation proph_map.
+From iris.heap_lang Require Import proofmode notation.
+From iris.base_logic.lib Require Import proph_map.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
diff --git a/theories/heap_lang/lib/coin_flip.v b/theories/heap_lang/lib/coin_flip.v
index 7e3569b1eb12564cb7d097c37992a63ecffeb34e..2f76409d2cc2bf950ec72dba623569dcbc0a8908 100644
--- a/theories/heap_lang/lib/coin_flip.v
+++ b/theories/heap_lang/lib/coin_flip.v
@@ -61,10 +61,10 @@ Section coinflip.
     iModIntro. wp_seq. done.
   Qed.
 
-  Definition val_to_bool (v : option val) : bool :=
+  Definition val_list_to_bool (v : list val) : bool :=
     match v with
-    | Some (LitV (LitBool b)) => b
-    | _                       => true
+    | LitV (LitBool b) :: _ => b
+    | _                     => true
     end.
 
   Lemma lateChoice_spec (x: loc) :
@@ -81,11 +81,11 @@ Section coinflip.
     iMod "AU" as "[Hl [_ Hclose]]".
     iDestruct "Hl" as (v') "Hl".
     wp_store.
-    iMod ("Hclose" $! (val_to_bool v) with "[Hl]") as "HΦ"; first by eauto.
+    iMod ("Hclose" $! (val_list_to_bool v) with "[Hl]") as "HΦ"; first by eauto.
     iModIntro. wp_apply rand_spec; try done.
     iIntros (b') "_".
     wp_apply (wp_resolve_proph with "Hp").
-    iIntros (->). wp_seq. done.
+    iIntros (vs) "[HEq _]". iDestruct "HEq" as "->". wp_seq. done.
   Qed.
 
 End coinflip.
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 4d3b6326702ae1895bce30a17e5b641bcd3fe361..8974f96faeb0f98840bfde988202f963956d1da9 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -1,8 +1,9 @@
 From iris.algebra Require Import auth gmap.
 From iris.base_logic Require Export gen_heap.
+From iris.base_logic.lib Require Export proph_map.
 From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
-From iris.heap_lang Require Export lang proph_map.
+From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics.
 From iris.proofmode Require Import tactics.
 From stdpp Require Import fin_maps.
@@ -308,39 +309,30 @@ Proof.
   iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
 
-(** Lifting lemmas for creating and resolving prophecy variables *)
-Lemma wp_new_proph :
-  {{{ True }}} NewProph {{{ v (p : proph_id), RET (LitV (LitProphecy p)); proph p v }}}.
+Lemma wp_new_proph s E :
+  {{{ True }}}
+    NewProph @ s; E
+  {{{ vs p, RET (LitV (LitProphecy p)); proph p vs }}}.
 Proof.
   iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κ κs n) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
-  iSplit; first by eauto.
+  iIntros (σ1 κ κs n) "[Hσ HR] !>". iSplit; first by eauto.
   iNext; iIntros (v2 σ2 efs Hstep). inv_head_step.
-  iMod (@proph_map_alloc with "HR") as "[HR Hp]".
-  { intro Hin. apply (iffLR (elem_of_subseteq _ _) Hdom) in Hin. done. }
-  iModIntro; iSplit=> //. iFrame. iSplitL "HR".
-  - iExists _. iSplit; last done.
-    iPureIntro. split.
-    + apply first_resolve_insert; auto.
-    + rewrite dom_insert_L. by apply union_mono_l.
-  - iApply "HΦ". done.
+  iMod (proph_map_new_proph p with "HR") as "[HR Hp]"; first done.
+  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 
-Lemma wp_resolve_proph p v w:
-  {{{ proph p v }}}
-    ResolveProph (Val $ LitV $ LitProphecy p) (Val w)
-  {{{ RET (LitV LitUnit); ⌜v = Some w⌝ }}}.
+Lemma wp_resolve_proph s E p vs v :
+  {{{ proph p vs }}}
+    ResolveProph (Val $ LitV $ LitProphecy p) (Val v) @ s; E
+  {{{ vs', RET (LitV LitUnit); ⌜vs = v::vs'⌝ ∗ proph p vs' }}}.
 Proof.
   iIntros (Φ) "Hp HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κ κs n) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
-  iDestruct (@proph_map_valid with "HR Hp") as %Hlookup.
-  iSplit; first by eauto.
-  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. iApply fupd_frame_l.
-  iSplit=> //. iFrame.
-  iMod (@proph_map_remove with "HR Hp") as "Hp". iModIntro.
-  iSplitR "HΦ".
-  - iExists _. iFrame. iPureIntro. split; first by eapply first_resolve_delete.
-    rewrite dom_delete. set_solver.
-  - iApply "HΦ". iPureIntro. by eapply first_resolve_eq.
+  iIntros (σ1 κ κs n) "[Hσ HR] !>". iSplit; first by eauto.
+  iNext; iIntros (v2 σ2 efs Hstep). inv_head_step.
+  iMod (proph_map_resolve_proph p v κs with "[HR Hp]") as "HPost"; first by iFrame.
+  iModIntro. iFrame. iSplitR; first done.
+  iDestruct "HPost" as (vs') "[HEq [HR Hp]]". iFrame.
+  iApply "HΦ". iFrame.
 Qed.
+
 End lifting.
diff --git a/theories/heap_lang/proph_map.v b/theories/heap_lang/proph_map.v
deleted file mode 100644
index 4e965dd67cff9f4b82bd172d3955447573f76b81..0000000000000000000000000000000000000000
--- a/theories/heap_lang/proph_map.v
+++ /dev/null
@@ -1,175 +0,0 @@
-From iris.algebra Require Import auth gmap.
-From iris.base_logic.lib Require Export own.
-From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
-Import uPred.
-
-Definition proph_map (P V : Type) `{Countable P} := gmap P (option V).
-Definition proph_val_list (P V : Type) := list (P * V).
-
-Definition proph_mapUR (P V : Type) `{Countable P} : ucmraT :=
-  gmapUR P $ exclR $ optionC $ leibnizC V.
-
-Definition to_proph_map {P V} `{Countable P} (pvs : proph_map P V) : proph_mapUR P V :=
-  fmap (λ v, Excl (v : option (leibnizC V))) pvs.
-
-(** The CMRA we need. *)
-Class proph_mapG (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapG {
-  proph_map_inG :> inG Σ (authR (proph_mapUR P V));
-  proph_map_name : gname
-}.
-Arguments proph_map_name {_ _ _ _ _} _ : assert.
-
-Class proph_mapPreG (P V : Type) (Σ : gFunctors) `{Countable P} :=
-  { proph_map_preG_inG :> inG Σ (authR (proph_mapUR P V)) }.
-
-Definition proph_mapΣ (P V : Type) `{Countable P} : gFunctors :=
-  #[GFunctor (authR (proph_mapUR P V))].
-
-Instance subG_proph_mapPreG {Σ P V} `{Countable P} :
-  subG (proph_mapΣ P V) Σ → proph_mapPreG P V Σ.
-Proof. solve_inG. Qed.
-
-Section definitions.
-  Context `{Countable P, pG : !proph_mapG P V Σ}.
-
-  (** The first resolve for [p] in [pvs] *)
-  Definition first_resolve (pvs : proph_val_list P V) (p : P) : option V :=
-    (list_to_map pvs : gmap P V) !! p.
-
-  Definition first_resolve_in_list (R : proph_map P V) (pvs : proph_val_list P V) :=
-    ∀ p v, p ∈ dom (gset _) R →
-           first_resolve pvs p = Some v →
-           R !! p = Some (Some v).
-
-  Definition proph_map_auth (R : proph_map P V) : iProp Σ :=
-    own (proph_map_name pG) (● (to_proph_map R)).
-
-  Definition proph_map_ctx (pvs : proph_val_list P V) (ps : gset P) : iProp Σ :=
-    (∃ R, ⌜first_resolve_in_list R pvs ∧
-          dom (gset _) R ⊆ ps⌝ ∗
-          proph_map_auth R)%I.
-
-  Definition proph_def (p : P) (v: option V) : iProp Σ :=
-    own (proph_map_name pG) (â—¯ {[ p := Excl (v : option $ leibnizC V) ]}).
-  Definition proph_aux : seal (@proph_def). by eexists. Qed.
-  Definition proph := proph_aux.(unseal).
-  Definition proph_eq :
-    @proph = @proph_def := proph_aux.(seal_eq).
-End definitions.
-
-Section first_resolve.
-  Context {P V : Type} `{Countable P}.
-  Implicit Type pvs : proph_val_list P V.
-  Implicit Type p : P.
-  Implicit Type v : V.
-  Implicit Type R : proph_map P V.
-
-  Lemma first_resolve_insert pvs p R :
-    first_resolve_in_list R pvs →
-    p ∉ dom (gset _) R →
-    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].
-    - 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 :
-    first_resolve_in_list R ((p, v) :: pvs) →
-    first_resolve_in_list (delete p R) pvs.
-  Proof.
-    intros Hfr p' v' Hpin Heq. rewrite dom_delete_L in Hpin. rewrite /first_resolve in Heq.
-    apply elem_of_difference in Hpin as [Hpin Hne%not_elem_of_singleton].
-    erewrite <- lookup_insert_ne in Heq; last done. rewrite lookup_delete_ne; eauto.
-  Qed.
-
-  Lemma first_resolve_eq R p v w pvs :
-    first_resolve_in_list R ((p, v) :: pvs) →
-    R !! p = Some w →
-    w = Some v.
-  Proof.
-    intros Hfr Hlookup. specialize (Hfr p v (elem_of_dom_2 _ _ _ Hlookup)).
-    rewrite /first_resolve lookup_insert in Hfr. rewrite Hfr in Hlookup; last done.
-    inversion Hlookup. done.
-  Qed.
-
-End first_resolve.
-
-Section to_proph_map.
-  Context (P V : Type) `{Countable P}.
-  Implicit Types p : P.
-  Implicit Types R : proph_map P V.
-
-  Lemma to_proph_map_valid R : ✓ to_proph_map R.
-  Proof. intros l. rewrite lookup_fmap. by case (R !! l). Qed.
-
-  Lemma to_proph_map_insert p v R :
-    to_proph_map (<[p := v]> R) = <[p := Excl (v: option (leibnizC V))]> (to_proph_map R).
-  Proof. by rewrite /to_proph_map fmap_insert. Qed.
-
-  Lemma to_proph_map_delete p R :
-    to_proph_map (delete p R) = delete p (to_proph_map R).
-  Proof. by rewrite /to_proph_map fmap_delete. Qed.
-
-  Lemma lookup_to_proph_map_None R p :
-    R !! p = None → to_proph_map R !! p = None.
-  Proof. by rewrite /to_proph_map lookup_fmap=> ->. Qed.
-
-  Lemma proph_map_singleton_included R p v :
-    {[p := Excl v]} ≼ to_proph_map R → R !! p = Some v.
-  Proof.
-    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.
-
-
-Lemma proph_map_init `{Countable P, !proph_mapPreG P V PVS} pvs ps :
-  (|==> ∃ _ : proph_mapG P V PVS, proph_map_ctx pvs ps)%I.
-Proof.
-  iMod (own_alloc (● to_proph_map ∅)) as (γ) "Hh".
-  { apply: auth_auth_valid. exact: to_proph_map_valid. }
-  iModIntro. iExists (ProphMapG P V PVS _ _ _ γ), ∅. iSplit; last by iFrame.
-  iPureIntro. split =>//.
-Qed.
-
-Section proph_map.
-  Context `{Countable P, !proph_mapG P V Σ}.
-  Implicit Types p : P.
-  Implicit Types v : option V.
-  Implicit Types R : proph_map P V.
-
-  (** General properties of mapsto *)
-  Global Instance proph_timeless p v : Timeless (proph p v).
-  Proof. rewrite proph_eq /proph_def. apply _. Qed.
-
-  Lemma proph_map_alloc R p v :
-    p ∉ dom (gset _) R →
-    proph_map_auth R ==∗ proph_map_auth (<[p := v]> R) ∗ proph p v.
-  Proof.
-    iIntros (Hp) "HR". rewrite /proph_map_ctx proph_eq /proph_def.
-    iMod (own_update with "HR") as "[HR Hl]".
-    { eapply auth_update_alloc,
-        (alloc_singleton_local_update _ _ (Excl $ (v : option (leibnizC _))))=> //.
-      apply lookup_to_proph_map_None. apply (iffLR (not_elem_of_dom _ _) Hp). }
-    iModIntro. rewrite /proph_map_auth to_proph_map_insert. iFrame.
-  Qed.
-
-  Lemma proph_map_remove R p v :
-    proph_map_auth R -∗ proph p v ==∗ proph_map_auth (delete p R).
-  Proof.
-    iIntros "HR Hp". rewrite /proph_map_ctx proph_eq /proph_def.
-    rewrite /proph_map_auth to_proph_map_delete. iApply (own_update_2 with "HR Hp").
-    apply auth_update_dealloc, (delete_singleton_local_update _ _ _).
-  Qed.
-
-  Lemma proph_map_valid R p v : proph_map_auth R -∗ proph p v -∗ ⌜R !! p = Some v⌝.
-  Proof.
-    iIntros "HR Hp". rewrite /proph_map_ctx proph_eq /proph_def.
-    iDestruct (own_valid_2 with "HR Hp")
-      as %[HH%proph_map_singleton_included _]%auth_valid_discrete_2; auto.
-  Qed.
-End proph_map.