diff --git a/_CoqProject b/_CoqProject
index 610855d37c09234069840a50a2b782a748a7d146..629806fa8d921947362fb4092f911138b84f801b 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -88,7 +88,6 @@ 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/prophecy.v
 theories/heap_lang/lib/spawn.v
 theories/heap_lang/lib/par.v
 theories/heap_lang/lib/assert.v
diff --git a/theories/heap_lang/lib/atomic_snapshot.v b/theories/heap_lang/lib/atomic_snapshot.v
index a70db18090aeedc5b3b1feb989adf173ac84f770..d9dec1afa1bbd72ff604b06bd85267dc62b49735 100644
--- a/theories/heap_lang/lib/atomic_snapshot.v
+++ b/theories/heap_lang/lib/atomic_snapshot.v
@@ -3,7 +3,7 @@ From iris.heap_lang Require Export lifting notation.
 From iris.base_logic.lib Require Export invariants.
 From iris.program_logic Require Export atomic.
 From iris.proofmode Require Import tactics.
-From iris.heap_lang Require Import proofmode notation par prophecy.
+From iris.heap_lang Require Import proofmode notation par.
 From iris.bi.lib Require Import fractional.
 Set Default Proof Using "Type".
 
@@ -100,15 +100,15 @@ Section atomic_snapshot.
         then (Fst "x", Fst "y")
         else  "readPair" "l".
 
-  Definition readPair_proph pr : val :=
+  Definition readPair_proph : val :=
     rec: "readPair" "l" :=
       let: "xv1"    := readX "l"           in
-      let: "proph"  := new_prophecy pr #() in
+      let: "proph"  := new prophecy        in
       let: "y"      := readY "l"           in
       let: "xv2"    := readX "l"           in
       let: "v2"     := Snd "xv2"           in
       let: "v_eq"   := Snd "xv1" = "v2"    in
-      resolve_prophecy pr "proph" "v_eq" ;;
+      resolve "proph" to "v_eq" ;;
       if: "v_eq"
         then (Fst "xv1", "y")
       else "readPair" "l".
@@ -368,18 +368,16 @@ Section atomic_snapshot.
     wp_load. eauto.
   Qed.
 
-  Definition val_to_bool (v:val) : bool :=
+  Definition val_to_bool (v : option val) : bool :=
     match v with
-    | LitV (LitBool b) => b
-    | _                => false
+    | Some (LitV (LitBool b)) => b
+    | _                       => false
     end.
 
-  Variable pr: prophecy.
-
   Lemma readPair_spec γ p :
     is_pair γ p -∗
     <<< ∀ v1 v2 : val, pair_content γ (v1, v2) >>>
-       readPair_proph pr p
+       readPair_proph p
        @ ⊤∖↑N
     <<< pair_content γ (v1, v2), RET (v1, v2) >>>.
   Proof.
@@ -405,7 +403,7 @@ Section atomic_snapshot.
       }
     wp_load. wp_let.
     (* ************ new prophecy ********** *)
-    wp_apply new_prophecy_spec; first done.
+    wp_apply wp_new_proph; first done.
     iIntros (proph) "Hpr". iDestruct "Hpr" as (proph_val) "Hpr".
     wp_let.
     (* ************ readY ********** *)
@@ -447,7 +445,7 @@ Section atomic_snapshot.
         iNext. unfold pair_inv. eauto 8 with iFrame.
       }
       wp_load. wp_let. wp_proj. wp_let. wp_proj. wp_op.
-      case_bool_decide; wp_let; wp_apply (resolve_prophecy_spec with "Hpr");
+      case_bool_decide; wp_let; wp_apply (wp_resolve_proph with "Hpr");
         iIntros (->); wp_seq; wp_if.
       + inversion H; subst; clear H. wp_proj.
         assert (v_x2 = v_y) as ->. {
@@ -483,7 +481,7 @@ Section atomic_snapshot.
         iNext. unfold pair_inv. eauto 8 with iFrame.
       }
       wp_load. repeat (wp_let; wp_proj). wp_op. wp_let.
-      wp_apply (resolve_prophecy_spec with "Hpr").
+      wp_apply (wp_resolve_proph with "Hpr").
       iIntros (Heq). subst.
       case_bool_decide.
       + inversion H; subst; clear H. inversion Hproph.
diff --git a/theories/heap_lang/lib/atomic_snapshot_spec.v b/theories/heap_lang/lib/atomic_snapshot_spec.v
index 679975031934cab5944e482c97792397feeb0666..65b8911678988eb710f6a40a206b0c09384d90ea 100644
--- a/theories/heap_lang/lib/atomic_snapshot_spec.v
+++ b/theories/heap_lang/lib/atomic_snapshot_spec.v
@@ -3,7 +3,7 @@ From iris.heap_lang Require Export lifting notation.
 From iris.base_logic.lib Require Export invariants.
 From iris.program_logic Require Export atomic.
 From iris.proofmode Require Import tactics.
-From iris.heap_lang Require Import proofmode notation par prophecy.
+From iris.heap_lang Require Import proofmode notation par.
 From iris.bi.lib Require Import fractional.
 Set Default Proof Using "Type".
 
diff --git a/theories/heap_lang/lib/coin_flip.v b/theories/heap_lang/lib/coin_flip.v
index af0bf13cc1e05409f0a57aec105c6b9b78a9870b..514743a48d7651f255d4c768fbace12257447c47 100644
--- a/theories/heap_lang/lib/coin_flip.v
+++ b/theories/heap_lang/lib/coin_flip.v
@@ -4,7 +4,6 @@ From iris.program_logic Require Export atomic.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation par.
 From iris.bi.lib Require Import fractional.
-From iris.heap_lang Require Import prophecy.
 Set Default Proof Using "Type".
 
 (** Nondeterminism and Speculation:
@@ -29,19 +28,19 @@ Section coinflip.
     λ: "x",
     "x" <- #0 ;;
      rand #().
-    
+
   Context `{!heapG Σ} (N: namespace).
-  
+
   Lemma rand_spec :
     {{{ True }}} rand #() {{{ (b : bool), RET #b; True }}}.
   Proof using N.
     iIntros (Φ) "_ HP".
     wp_lam. wp_alloc l as "Hl". wp_lam.
     iMod (inv_alloc N _ (∃ (b: bool), l ↦ #b)%I with "[Hl]") as "#Hinv"; first by eauto.
-    wp_apply wp_fork. iSplitL.
+    wp_apply wp_fork.
+    - iInv N as (b) ">Hl". wp_store. iModIntro. iSplitL; eauto.
     - wp_lam. iInv N as (b) ">Hl". wp_load. iModIntro. iSplitL "Hl"; first by eauto.
       iApply "HP". done.
-    - iInv N as (b) ">Hl". wp_store. iModIntro. iSplitL; eauto.    
   Qed.
 
   Lemma earlyChoice_spec (x: loc) :
@@ -50,7 +49,7 @@ Section coinflip.
         @ ⊤
     <<< ∃ (b: bool), x ↦ #0, RET #b >>>.
   Proof using N.
-    iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.    
+    iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
     wp_bind (rand _)%E. iApply rand_spec; first done.
     iIntros (b) "!> _". wp_let.
     wp_bind (_ <- _)%E.
@@ -78,47 +77,48 @@ Section coinflip.
     iMod ("Hclose" $! true with "[Hl]") as "AU"; first by eauto.
     iModIntro. wp_seq.
     iApply rand_spec; first done.
-    iIntros (b) "!> _".    
+    iIntros (b) "!> _".
     Abort.
 
 End coinflip.
 
-Section coinflip_with_prophecy.  
-    
-  Context `{!heapG Σ} `{pr: prophecy} (N: namespace).
+Section coinflip_with_prophecy.
+
+  Context `{!heapG Σ} (N: namespace).
 
   Definition val_to_bool v : bool :=
     match v with
-    | LitV (LitBool b) => b
-    | _                => true
+    | Some (LitV (LitBool b)) => b
+    | _                       => true
     end.
 
   Definition lateChoice_proph: val :=
     λ: "x",
-      let: "p" := new_prophecy pr #() in
+      let: "p" := new prophecy in
       "x" <- #0 ;;
       let: "r" := rand #() in
-      resolve_prophecy pr "p" "r".
-  
+      resolve "p" to "r" ;;
+      "r".
+
   Lemma lateChoice_proph_spec (x: loc) :
     <<< x ↦ - >>>
         lateChoice_proph #x
         @ ⊤
-    <<< ∃ (b: bool), x ↦ #0, RET #b >>>. 
+    <<< ∃ (b: bool), x ↦ #0, RET #b >>>.
   Proof using N.
     iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
-    wp_apply new_prophecy_spec; first done.
+    wp_apply wp_new_proph; first done.
     iIntros (p) "Hp". iDestruct "Hp" as (v) "Hp".
-    wp_let.    
+    wp_let.
     wp_bind (_ <- _)%E.
     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.
     iModIntro. wp_seq. wp_apply rand_spec; try done.
-    iIntros (b') "_". wp_let.
-    iApply (resolve_prophecy_spec with "Hp").
-    iNext. iIntros (->). done.
+    iIntros (b') "_". wp_let. wp_bind (resolve _ to _)%E.
+    iApply (wp_resolve_proph with "Hp").
+    iNext. iIntros (->). wp_seq. done.
   Qed.
 
 End coinflip_with_prophecy.
diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index f385c27380a15e1a2610491e63b869cb5150b960..596479602f94ed97fed5729c0738176dfa87cdb5 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -157,3 +157,6 @@ Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
 Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" :=
   (Match e0 BAnon e1 x%bind e2)
   (e0, e1, x, e2 at level 200, only parsing) : expr_scope.
+
+Notation "'new' 'prophecy'" := NewProph (at level 100) : expr_scope.
+Notation "'resolve' p 'to' v" := (ResolveProph p v) (at level 100) : expr_scope.
diff --git a/theories/heap_lang/prophecy.v b/theories/heap_lang/prophecy.v
deleted file mode 100644
index 2e7af6544383bbbc21afc555c0a69abc914e9510..0000000000000000000000000000000000000000
--- a/theories/heap_lang/prophecy.v
+++ /dev/null
@@ -1,27 +0,0 @@
-From iris.heap_lang Require Export lifting notation.
-From iris.base_logic.lib Require Export invariants.
-From iris.program_logic Require Export atomic.
-From iris.proofmode Require Import tactics.
-From iris.heap_lang Require Import proofmode notation par.
-From iris.bi.lib Require Import fractional.
-Set Default Proof Using "Type".
-
-Section prophecy.
-
-  Context `{!heapG Σ} (N: namespace).
-
-  Record prophecy {Σ} `{!heapG Σ} := Prophecy {
-    (* -- operations -- *)
-    new_prophecy : val;
-    resolve_prophecy : val;
-    (* -- predicates -- *)
-    is_prophecy : proph -> val -> iProp Σ;
-    (* -- general properties -- *)
-    new_prophecy_spec:
-      {{{ True }}} new_prophecy #() {{{ p, RET #p; ∃ v, is_prophecy p v }}};
-    resolve_prophecy_spec p v e w:
-      IntoVal e w ->
-      {{{ is_prophecy p v }}} resolve_prophecy #p e {{{ RET w; ⌜v = w⌝ }}} 
-  }.
-
-End prophecy.
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 31e5c3a366f103685fb7e8f1ce0d237694cefeaa..5cf879d9d6995bc2ee7140a5a12cdd67c0c7bc30 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -35,7 +35,9 @@ Inductive expr :=
   | Load (e : expr)
   | Store (e1 : expr) (e2 : expr)
   | CAS (e0 : expr) (e1 : expr) (e2 : expr)
-  | FAA (e1 : expr) (e2 : expr).
+  | FAA (e1 : expr) (e2 : expr)
+  | NewProph
+  | ResolveProph (e1 : expr) (e2 : expr).
 
 Fixpoint to_expr (e : expr) : heap_lang.expr :=
   match e with
@@ -60,6 +62,8 @@ Fixpoint to_expr (e : expr) : heap_lang.expr :=
   | Store e1 e2 => heap_lang.Store (to_expr e1) (to_expr e2)
   | CAS e0 e1 e2 => heap_lang.CAS (to_expr e0) (to_expr e1) (to_expr e2)
   | FAA e1 e2 => heap_lang.FAA (to_expr e1) (to_expr e2)
+  | NewProph => heap_lang.NewProph
+  | ResolveProph e1 e2 => heap_lang.ResolveProph (to_expr e1) (to_expr e2)
   end.
 
 Ltac of_expr e :=
@@ -93,7 +97,11 @@ Ltac of_expr e :=
      let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
      constr:(CAS e0 e1 e2)
   | heap_lang.FAA ?e1 ?e2 =>
-     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(FAA e1 e2)
+    let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(FAA e1 e2)
+  | heap_lang.NewProph =>
+    constr:(NewProph)
+  | heap_lang.ResolveProph ?e1 ?e2 =>
+    let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(ResolveProph e1 e2)
   | to_expr ?e => e
   | of_val ?v => constr:(Val v (of_val v) (to_of_val v))
   | language.of_val ?v => constr:(Val v (of_val v) (to_of_val v))
@@ -108,10 +116,10 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
   | Val _ _ _ | ClosedExpr _ => true
   | Var x => bool_decide (x ∈ X)
   | Rec f x e => is_closed (f :b: x :b: X) e
-  | Lit _ => true
+  | Lit _ | NewProph => true
   | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e =>
      is_closed X e
-  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 =>
+  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 | ResolveProph e1 e2 =>
      is_closed X e1 && is_closed X e2
   | If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
      is_closed X e0 && is_closed X e1 && is_closed X e2
@@ -171,6 +179,8 @@ Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
   | Store e1 e2 => Store (subst x es e1) (subst x es e2)
   | CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
   | FAA e1 e2 => FAA (subst x es e1) (subst x es e2)
+  | NewProph => NewProph
+  | ResolveProph e1 e2 => ResolveProph (subst x es e1) (subst x es e2)
   end.
 Lemma to_expr_subst x er e :
   to_expr (subst x er e) = heap_lang.subst x (to_expr er) (to_expr e).
@@ -190,6 +200,8 @@ Definition is_atomic (e : expr) :=
   | Fork _ => true
   (* Make "skip" atomic *)
   | App (Rec _ _ (Lit _)) (Lit _) => true
+  | NewProph => true
+  | ResolveProph e1 e2 => bool_decide (is_Some (to_val e1) ∧ is_Some (to_val e2))
   | _ => false
   end.
 Lemma is_atomic_correct s e : is_atomic e → Atomic s (to_expr e).
@@ -293,4 +305,6 @@ Ltac reshape_expr e tac :=
   | CAS ?e0 ?e1 ?e2 => go (CasRCtx e0 e1 :: K) e2
   | FAA ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => go (FaaLCtx v2 :: K) e1)
   | FAA ?e1 ?e2 => go (FaaRCtx e1 :: K) e2
+  | ResolveProph ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => go (ProphLCtx v2 :: K) e1)
+  | ResolveProph ?e1 ?e2 => go (ProphRCtx e1 :: K) e2
   end in go (@nil ectx_item) e.