diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index a5f0b688836ee34b189848b05d7444bc9ecb1a32..d23688a932c0bfee920c80ffa283fe117f84ae05 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -23,9 +23,10 @@ Open Scope Z_scope.
 
 (** Expressions and vals. *)
 Definition loc := positive. (* Really, any countable type. *)
+Definition proph := positive.
 
 Inductive base_lit : Set :=
-  | LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitLoc (l : loc).
+  | LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitLoc (l : loc) | LitProphecy (p: proph).
 Inductive un_op : Set :=
   | NegOp | MinusUnOp.
 Inductive bin_op : Set :=
@@ -192,11 +193,13 @@ Defined.
 Instance base_lit_countable : Countable base_lit.
 Proof.
  refine (inj_countable' (λ l, match l with
-  | LitInt n => inl (inl n) | LitBool b => inl (inr b)
-  | LitUnit => inr (inl ()) | LitLoc l => inr (inr l)
+  | LitInt n => (inl (inl n), None) | LitBool b => (inl (inr b), None)
+  | LitUnit => (inr (inl ()), None) | LitLoc l => (inr (inr l), None)
+  | LitProphecy p => (inr (inl ()), Some p)
   end) (λ l, match l with
-  | inl (inl n) => LitInt n | inl (inr b) => LitBool b
-  | inr (inl ()) => LitUnit | inr (inr l) => LitLoc l
+  | (inl (inl n), None) => LitInt n | (inl (inr b), None) => LitBool b
+  | (inr (inl ()), None) => LitUnit | (inr (inr l), None) => LitLoc l
+  | (_, Some p) => LitProphecy p                                                                 
   end) _); by intros [].
 Qed.
 Instance un_op_finite : Countable un_op.
diff --git a/theories/heap_lang/lib/coin-flip.v b/theories/heap_lang/lib/coin-flip.v
new file mode 100644
index 0000000000000000000000000000000000000000..d540ccae212719aff7f99fd027db67c05495669a
--- /dev/null
+++ b/theories/heap_lang/lib/coin-flip.v
@@ -0,0 +1,151 @@
+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".
+
+(** Nondeterminism and Speculation:
+    Implementing "Late choice versus early choice" example from
+    Logical Relations for Fine-Grained Concurrency by Turon et al. (POPL'13) *)
+
+Definition rand: val :=
+    λ: "_",
+       let: "y" := ref #false in
+       Fork ("y" <- #true) ;;
+       !"y".
+
+  Definition earlyChoice: val :=
+    λ: "x",
+       let: "r" := rand #() in
+       "x" <- #0 ;;
+       "r".
+
+Section coinflip.
+
+  Definition lateChoice: val :=
+    λ: "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_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) :
+    <<< x ↦ - >>>
+        earlyChoice #x
+        @ ⊤
+    <<< ∃ (b: bool), x ↦ #0, RET #b >>>.
+  Proof using N.
+    iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.    
+    wp_bind (rand _)%E. iApply rand_spec; first done.
+    iIntros (b) "!> _". wp_let.
+    wp_bind (_ <- _)%E.
+    iMod "AU" as "[Hl [_ Hclose]]".
+    iDestruct "Hl" as (v) "Hl".
+    wp_store.
+    iMod ("Hclose" with "[Hl]") as "HΦ"; first by eauto.
+    iModIntro. wp_seq. done.
+  Qed.
+
+  (* lateChoice can currently not be proved in Iris *)
+  Lemma lateChoice_spec (x: loc) :
+    <<< x ↦ - >>>
+        lateChoice #x
+        @ ⊤
+    <<< ∃ (b: bool), x ↦ #0, RET #b >>>.
+  Proof using N.
+    iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
+    wp_bind (_ <- _)%E.
+    iMod "AU" as "[Hl [_ Hclose]]".
+    iDestruct "Hl" as (v) "Hl".
+    wp_store.
+    (* now we have to "predict" the value of b, which is the result of calling rand.
+       but we can't know at this point what that value is. *)
+    iMod ("Hclose" $! true with "[Hl]") as "AU"; first by eauto.
+    iModIntro. wp_seq.
+    iApply rand_spec; first done.
+    iIntros (b) "!> _".    
+    Abort.
+
+End coinflip.
+
+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 w :
+      {{{ is_prophecy p v }}} resolve_prophecy #p w {{{ RET w; ⌜v = w⌝ }}} 
+  }.
+    
+  Context `{pr: prophecy}.
+
+  Definition lateChoice_proph: val :=
+    λ: "x",
+      let: "p" := new_prophecy pr #() in
+      "x" <- #0 ;;
+      let: "r" := rand #() in
+      resolve_prophecy pr "p" "r".
+
+  Definition val_to_bool v :=
+    match v with
+    | LitBool b => Some b
+    | _         => None
+    end.
+  
+  Lemma lateChoice_proph_spec (x: loc) :
+    <<< x ↦ - >>>
+        lateChoice_proph #x
+        @ ⊤
+    <<< ∃ (b: bool), x ↦ #0, RET #b >>>. 
+  Proof using N.
+    iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
+    wp_apply new_prophecy_spec; first done.
+    iIntros (p) "Hp". iDestruct "Hp" as (v) "Hp".
+    wp_let.    
+    wp_bind (_ <- _)%E.
+    iMod "AU" as "[Hl [_ Hclose]]".
+    iDestruct "Hl" as (v') "Hl".
+    wp_store.
+    destruct (val_to_bool v) eqn:Heq.
+    - iMod ("Hclose" $! b with "[Hl]") as "HΦ"; first by eauto.
+      iModIntro. wp_seq. wp_apply rand_spec; try done.
+      iIntros (b') "_". wp_let.
+      iDestruct (resolve_prophecy_spec with "Hp") as "Hs".
+      iAssert (▷(⌜#v = #b'⌝ -∗ Φ #b'))%I with "[HΦ]" as "Hb". {
+        iNext. iIntros "Heq". destruct v; inversion Heq; subst. iDestruct "Heq" as %->. done.
+      }
+      iSpecialize ("Hs" with "Hb"). done.
+    - iMod ("Hclose" $! true with "[Hl]") as "HΦ"; first by eauto.
+      iModIntro. wp_seq. wp_apply rand_spec; try done.
+      iIntros (b') "_". wp_let.
+      iDestruct (resolve_prophecy_spec with "Hp") as "Hs". 
+      iAssert (▷(⌜#v = #b'⌝ -∗ Φ #b'))%I with "[HΦ]" as "Hb". {
+        iNext. iIntros "Heq". iDestruct "Heq" as %[=Heq'].
+        destruct v; inversion Heq; inversion Heq'.
+      }
+      iSpecialize ("Hs" with "Hb"). done.
+  Qed.
+
+End prophecy.
diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index f8ef7a58517e001c25d35b3bcbeccdcbc9714547..f385c27380a15e1a2610491e63b869cb5150b960 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -8,6 +8,7 @@ Delimit Scope val_scope with V.
 Coercion LitInt : Z >-> base_lit.
 Coercion LitBool : bool >-> base_lit.
 Coercion LitLoc : loc >-> base_lit.
+Coercion LitProphecy : proph >-> base_lit.
 
 Coercion App : expr >-> Funclass.
 Coercion of_val : val >-> expr.