diff --git a/theories/examples/coinflip.v b/theories/examples/coinflip.v
index 6f9f11e5800fac06e1f4d6113f847f793c83b05f..af934a7539981b5b6ad5250bdd1a2a916f5077f0 100644
--- a/theories/examples/coinflip.v
+++ b/theories/examples/coinflip.v
@@ -19,8 +19,8 @@ Definition flip_lazy' : val := λ: "c" "lk" "p" <>,
 
 Definition read_lazy : val := rec: "read" "c" <> :=
   match: !"c" with
-    InjR "v" => "v"
-  | InjL <>  =>
+    SOME "v" => "v"
+  | NONE  =>
       let: "x" := rand #() in
       if: CAS "c" NONEV (SOME "x")
       then "x"
diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v
index e3d70b167cc0b7c32c57723837b1854de14a1ae2..d96628af0b07233b042124533c952d719c28d3d3 100644
--- a/theories/examples/symbol.v
+++ b/theories/examples/symbol.v
@@ -218,7 +218,7 @@ Section proof.
   Lemma refinement1 :
     REL symbol1 << symbol2 : () → lrel_symbol.
   Proof.
-    iApply refines_arrow_val; [done|done|].
+    iApply refines_arrow_val.
     iAlways. iIntros (? ?) "[% %]"; simplify_eq/=.
     rel_rec_l. rel_rec_r.
     rel_alloc_l size1 as "[Hs1 Hs1']"; repeat rel_pure_l.
@@ -297,7 +297,7 @@ Section proof.
   Lemma refinement2 :
     REL symbol2 << symbol1 : () → lrel_symbol.
   Proof.
-    iApply refines_arrow_val; [done|done|].
+    iApply refines_arrow_val.
     iAlways. iIntros (? ?) "[% %]"; simplify_eq/=.
     rel_rec_l. rel_rec_r.
     rel_alloc_l size1 as "[Hs1 Hs1']"; repeat rel_pure_l.
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index c4491dc6f6eec364445dbd61868b7e51055cdc2a..91557507302a4e5c2d0a94cfd598434f102b74c0 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -104,8 +104,8 @@ Section refinement.
   Lemma newlock_refinement :
     REL newlock << reloc.lib.lock.newlock : () → lockInt.
   Proof.
-    iApply refines_arrow_val; [done|done|].
-    iAlways. iIntros (? ?) "/= [% %]"; simplify_eq.
+    rel_arrow_val.
+    iIntros (? ?) "/= [% %]"; simplify_eq.
     (* Reducing to a value on the LHS *)
     rel_rec_l.
     rel_alloc_l ln as "Hln".
@@ -209,8 +209,8 @@ Section refinement.
   Lemma acquire_refinement :
     REL acquire << reloc.lib.lock.acquire : lockInt → ().
   Proof.
-    iApply refines_arrow_val; [done|done|].
-    iAlways. iIntros (? lk) "/= #Hl".
+    rel_arrow_val.
+    iIntros (? lk) "/= #Hl".
     iDestruct "Hl" as (lo ln γ) "(% & Hin)". simplify_eq/=.
     rel_apply_l (acquire_l_logatomic
                    (fun o => ∃ st, is_locked_r lk st ∗
@@ -241,8 +241,8 @@ Section refinement.
   Lemma acquire_refinement_direct :
     REL acquire << reloc.lib.lock.acquire : lockInt → ().
   Proof.
-    iApply refines_arrow_val; [done|done|].
-    iAlways. iIntros (? ?) "/= #Hl".
+    rel_arrow_val.
+    iIntros (? ?) "/= #Hl".
     iDestruct "Hl" as (lo ln γ) "(% & Hin)". simplify_eq.
     rel_rec_l. repeat rel_proj_l.
     rel_apply_l (FG_increment_atomic_l (issuedTickets γ)%I True%I); first done.
@@ -307,8 +307,8 @@ Section refinement.
   Lemma release_refinement :
     REL release << reloc.lib.lock.release : lockInt → ().
   Proof.
-    iApply refines_arrow_val; [done|done|].
-    iAlways. iIntros (? lk) "/= #Hl".
+    rel_arrow_val.
+    iIntros (? lk) "/= #Hl".
     iDestruct "Hl" as (lo ln γ) "(% & Hin)". simplify_eq.
     rel_rec_l. rel_proj_l.
     pose (R := fun (o : nat) =>
diff --git a/theories/logic/derived.v b/theories/logic/derived.v
index 431d95b5477a0459a6fe907455262d52fb6c8143..8b4082332c669f654b11788d5c715a4f69f92788 100644
--- a/theories/logic/derived.v
+++ b/theories/logic/derived.v
@@ -21,14 +21,12 @@ Section rules.
     by iApply "HAA".
   Qed.
 
-  Lemma refines_arrow v v' (f x f' x' : binder) (eb eb' : expr) A A' :
-    AsRecV v f x eb →
-    AsRecV v' f' x' eb' →
+  Lemma refines_arrow (v v' : val) A A' :
     □ (∀ v1 v2 : val, □(REL of_val v1 << of_val v2 : A) -∗
       REL App v (of_val v1) << App v' (of_val v2) : A') -∗
     REL v << v' : (A → A')%lrel.
   Proof.
-    iIntros (??) "#H".
+    iIntros "#H".
     iApply refines_arrow_val; eauto.
     iAlways. iIntros (v1 v2) "#HA".
     iApply "H". iAlways.
diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index 64205c6734a6405163f0f6633c727eb32a0dc7a5..98df0d515b1e5d69bd86194b89d2fb7f1f5fdebc 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -290,14 +290,12 @@ Section rules.
   Qed.
 
   (** This rule is useful for proving that functions refine each other *)
-  Lemma refines_arrow_val v v' (f x f' x' : binder) eb eb' A A' :
-    AsRecV v f x eb →
-    AsRecV v' f' x' eb' →
+  Lemma refines_arrow_val v v' A A' :
     □(∀ v1 v2, A v1 v2 -∗
       REL App v (of_val v1) << App v' (of_val v2) : A') -∗
     REL v << v' : (A → A')%lrel.
   Proof.
-    rewrite /AsRecV. iIntros (-> ->) "#H".
+    rewrite /AsRecV. iIntros "#H".
     iApply refines_spec_ctx. iIntros "Hs".
     iApply refines_ret. iModIntro.
     iModIntro. iIntros (v1 v2) "HA".