diff --git a/theories/examples/lateearlychoice.v b/theories/examples/lateearlychoice.v
index 05bdf7cf603785bc685c48714a997ab8b54508fd..ec29969f10153a30f5b73f4357700e8a76eb79ad 100644
--- a/theories/examples/lateearlychoice.v
+++ b/theories/examples/lateearlychoice.v
@@ -76,11 +76,9 @@ Section proof.
     iApply refines_arrow_val.
     iModIntro. iIntros (x x') "#Hxx".
     rel_rec_l. rel_rec_r.
-    rel_bind_l NewProph. iApply refines_wp_l.
-    iApply wp_new_proph; first done.
-    iNext. iIntros (v p) "Hp /=".
+    rel_newproph_l vs p as "Hp".
     repeat rel_pure_l.
-    rel_apply_r (refines_rand_r (val_to_bool v)).
+    rel_apply_r (refines_rand_r (val_to_bool vs)).
     repeat rel_pure_r.
     iApply (refines_seq lrel_unit).
     { iApply refines_store.
@@ -88,11 +86,9 @@ Section proof.
       - rel_values. }
     rel_apply_l refines_rand_l.
     iNext. iIntros (b). repeat rel_pure_l.
-    rel_bind_l (resolve_proph: _ to: _)%E.
-    iApply refines_wp_l.
-    iApply (wp_resolve_proph with "Hp"). iNext.
-    iIntros (vs') "[-> H]". iSimpl. repeat rel_pure_l.
-    rel_values.
+    rel_apply_l refines_resolveproph_l. iModIntro.
+    iExists _; iFrame. iNext. iIntros (vs' ->) "H".
+    repeat rel_pure_l. rel_values.
   Qed.
 
   Lemma early_late_choice :
@@ -119,8 +115,7 @@ Section proof.
     iApply refines_arrow_val.
     iModIntro. iIntros (x x') "#Hxx".
     rel_rec_l. rel_rec_r.
-    rel_apply_r refines_newproph_r.
-    iIntros (p). repeat rel_pure_r.
+    rel_newproph_r p. repeat rel_pure_r.
     iApply (refines_seq lrel_unit with "[Hxx]").
     { iApply refines_store.
       - iApply refines_ret. iApply "Hxx".
diff --git a/theories/logic/proofmode/tactics.v b/theories/logic/proofmode/tactics.v
index 3495eab538e9ff1f905d56691439339708609135..de21aa0083b071063f931baf8ae5729af9f720f9 100644
--- a/theories/logic/proofmode/tactics.v
+++ b/theories/logic/proofmode/tactics.v
@@ -506,6 +506,67 @@ Tactic Notation "rel_cas_suc_r" :=
   |reflexivity
   |rel_finish  (** new goal *)].
 
+(** NewProph *)
+Tactic Notation "rel_newproph_l_atomic" := rel_apply_l refines_newproph_l.
+
+Lemma tac_rel_newproph_l_simpl `{relocG Σ} K ℶ1 ℶ2 e t A :
+  e = fill K NewProph →
+  MaybeIntoLaterNEnvs 1 ℶ1 ℶ2 →
+  (envs_entails ℶ2 (∀ (vs : list val) (p : proph_id),
+     (proph p vs -∗ refines ⊤ (fill K (of_val #p)) t A))) →
+  envs_entails ℶ1 (refines ⊤ e t A).
+Proof.
+  rewrite envs_entails_eq. intros ???; subst.
+  rewrite into_laterN_env_sound /=.
+  rewrite -(refines_newproph_l _ ⊤); eauto.
+  rewrite -fupd_intro.
+  by apply bi.later_mono.
+Qed.
+
+Tactic Notation "rel_newproph_l" ident(p) ident(vs) "as" constr(H) :=
+  iStartProof;
+  first
+    [rel_reshape_cont_l ltac:(fun K e' =>
+       eapply (tac_rel_newproph_l_simpl K);
+       [reflexivity (** e = fill K (NewProph e') *)
+       |idtac..])
+    |fail 1 "rel_newproph_l: cannot find 'NewProph'"];
+  [iSolveTC                      (** IntoLaters *)
+  |iIntros (p vs) H; rel_finish  (** new goal *)].
+
+Lemma tac_rel_newproph_r `{relocG Σ} K' ℶ E e t A :
+  t = fill K' NewProph →
+  nclose specN ⊆ E →
+  envs_entails ℶ (∀ (p : proph_id), refines E e (fill K' #p) A) →
+  envs_entails ℶ (refines E e t A).
+Proof.
+  intros ???. subst t.
+  rewrite -refines_newproph_r //.
+Qed.
+
+Tactic Notation "rel_newproph_r" ident(p) :=
+  iStartProof;
+  first
+    [rel_reshape_cont_r ltac:(fun K e' =>
+       eapply (tac_rel_newproph_r K);
+       [reflexivity  (** t = K'[newproph] *)
+       |idtac..])
+    |fail 1 "rel_newproph_r: cannot find 'NewProph'"];
+  [solve_ndisj || fail "rel_newproph_r: cannot prove 'nclose specN ⊆ ?'"
+  |iIntros (p); rel_finish  (** new goal *)].
+
+Tactic Notation "rel_newproph_r" :=
+  let p := fresh in
+  rel_newproph_r p.
+
+Tactic Notation "rel_newproph_l" :=
+  let p := fresh in
+  let vs := fresh in
+  let H := iFresh "H" in
+  rel_newproph_l p vs as H.
+
+(** ResolveProph *)
+(* TODO: implement this lol *)
 
 (** Fork *)
 Lemma tac_rel_fork_l `{relocG Σ} K ℶ E e' eres e t A :
diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index 6136170920b29ec28f46766575ce038ab144c246..1aa8567bf6cbde11cbfdd1567103179de28e22b5 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -352,6 +352,33 @@ Section rules.
     iApply (wp_alloc _ _ v); auto.
   Qed.
 
+  Lemma refines_newproph_l K E t A :
+    (|={⊤,E}=> ▷ (∀ (vs : list val) (p : proph_id),
+           proph p vs -∗
+           REL fill K (of_val #p) << t @ E : A))%I
+    -∗ REL fill K NewProph << t : A.
+  Proof.
+    iIntros "Hlog".
+    iApply refines_atomic_l; auto.
+    iMod "Hlog". iModIntro.
+    iApply wp_new_proph=>//.
+  Qed.
+
+  Lemma refines_resolveproph_l K E (p : proph_id) w t A :
+    (|={⊤,E}=> ∃ vs,
+           ▷ (proph p vs) ∗
+           ▷ (∀ (vs' : list val), ⌜vs = w::vs'⌝ -∗
+                  proph p vs' -∗
+                  REL fill K (of_val #()) << t @ E : A))%I
+    -∗ REL fill K (ResolveProph #p w) << t : A.
+  Proof.
+    iIntros "Hlog".
+    iApply refines_atomic_l; auto.
+    iMod "Hlog" as (vs) "[>Hp Hlog]". iModIntro.
+    iApply (wp_resolve_proph with "Hp") =>//.
+    iNext. iIntros (vs'). by rewrite -bi.wand_curry.
+  Qed.
+
   Lemma refines_load_l K E l q t A :
     (|={⊤,E}=> ∃ v',
       ▷(l ↦{q} v') ∗