diff --git a/theories/examples/coinflip.v b/theories/examples/coinflip.v
index 7eaf54afca99c667e30971687f0687082748e5bf..c9745b63dabc6d0082e02e5a093188ab88df859f 100644
--- a/theories/examples/coinflip.v
+++ b/theories/examples/coinflip.v
@@ -148,7 +148,7 @@ Section proofs.
       iDestruct "H" as "[Hcl|Hcl]"; rel_load_r; repeat rel_pure_r.
       + rel_apply_r (refines_rand_r b). repeat rel_pure_r.
         rel_store_r. repeat rel_pure_r.
-        rel_apply_r refines_resolveproph_r. repeat rel_pure_r.
+        rel_resolveproph_r. repeat rel_pure_r.
         rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk".
         repeat rel_pure_r. iMod ("Hclose" with "[-]") as "_".
         { eauto with iFrame. }
@@ -281,7 +281,7 @@ Section proofs.
           iIntros "Hlk". repeat rel_pure_r. rel_load_r.
           repeat rel_pure_r. rel_apply_r (refines_rand_r b).
           repeat rel_pure_r. rel_store_r.
-          repeat rel_pure_r. rel_apply_r refines_resolveproph_r.
+          repeat rel_pure_r. rel_resolveproph_r.
           repeat rel_pure_r. rel_apply_r (refines_release_r with "Hlk").
           iIntros "Hlk". repeat rel_pure_r.
           iMod ("Hclose" with "[-]") as "_".
diff --git a/theories/examples/lateearlychoice.v b/theories/examples/lateearlychoice.v
index ec29969f10153a30f5b73f4357700e8a76eb79ad..1486e54c084fa201ee30f198a3f519827094c027 100644
--- a/theories/examples/lateearlychoice.v
+++ b/theories/examples/lateearlychoice.v
@@ -123,8 +123,7 @@ Section proof.
     rel_apply_l refines_rand_l.
     iNext. iIntros (b). repeat rel_pure_l.
     rel_apply_r (refines_rand_r b).
-    repeat rel_pure_r.
-    rel_apply_r refines_resolveproph_r.
+    repeat rel_pure_r. rel_resolveproph_r.
     repeat rel_pure_r. rel_values.
   Qed.
 
diff --git a/theories/logic/proofmode/tactics.v b/theories/logic/proofmode/tactics.v
index de21aa0083b071063f931baf8ae5729af9f720f9..cf2b55d91327317bd1668fe69d7cc849fc90ebad 100644
--- a/theories/logic/proofmode/tactics.v
+++ b/theories/logic/proofmode/tactics.v
@@ -567,6 +567,27 @@ Tactic Notation "rel_newproph_l" :=
 
 (** ResolveProph *)
 (* TODO: implement this lol *)
+Lemma tac_rel_resolveproph_r `{relocG Σ} K' ℶ E (p :proph_id) w e t A :
+  t = fill K' (ResolveProph #p (of_val w)) →
+  nclose specN ⊆ E →
+  envs_entails ℶ (refines E e (fill K' #()) A) →
+  envs_entails ℶ (refines E e t A).
+Proof.
+  intros ???. subst t.
+  rewrite -refines_resolveproph_r //.
+Qed.
+
+Tactic Notation "rel_resolveproph_r" :=
+  iStartProof;
+  first
+    [rel_reshape_cont_r ltac:(fun K e' =>
+       eapply (tac_rel_resolveproph_r K);
+       [reflexivity  (** t = K'[resolveproph] *)
+       |idtac..])
+    |fail 1 "rel_resolveproph_r: cannot find 'ResolveProph'"];
+  [solve_ndisj || fail "rel_resolveproph_r: cannot prove 'nclose specN ⊆ ?'"
+  |rel_finish  (** new goal *)].
+
 
 (** Fork *)
 Lemma tac_rel_fork_l `{relocG Σ} K ℶ E e' eres e t A :