diff --git a/theories/examples/bit.v b/theories/examples/bit.v
index 50fce0abcc42f215f09419cb2c9d6e4a1e901560..c677894b63ae0cf4bf4d9810c6c15f4610029d53 100644
--- a/theories/examples/bit.v
+++ b/theories/examples/bit.v
@@ -26,7 +26,7 @@ Section bit_refinement.
   Lemma bit_refinement Δ : ⊢ REL bit_bool << bit_nat : interp bitτ Δ.
   Proof.
     unfold bitτ; simpl.
-    iApply (refines_exists R).
+    iApply (refines_pack R).
     progress repeat iApply refines_pair.
     - rel_values.
     - unfold flip_nat. rel_pure_l.
diff --git a/theories/examples/cell.v b/theories/examples/cell.v
index bbdbc55652cbf2384c3029709f502e844dffbe97..97d00a977b82bf5972fb79467b49ae3f068dea73 100644
--- a/theories/examples/cell.v
+++ b/theories/examples/cell.v
@@ -58,7 +58,7 @@ Section cell_refinement.
   Proof.
     unfold cell1, cell2.
     iApply refines_forall. iIntros "!#" (R).
-    iApply (refines_exists (cellR R)).
+    iApply (refines_pack (cellR R)).
     repeat iApply refines_pair.
     - (* New cell *)
       rel_pure_l. rel_pure_r.
diff --git a/theories/examples/namegen.v b/theories/examples/namegen.v
index 2f86e688d645154a48ed4e41b0e21c6ccb2d2d29..3dfe5cf8dee8d9c77f60333ed79091611d165b4f 100644
--- a/theories/examples/namegen.v
+++ b/theories/examples/namegen.v
@@ -47,7 +47,7 @@ Section namegen_refinement.
     iMod (inv_alloc N _ (ng_Inv γ c) with "[-]") as "#Hinv".
     { iNext. iExists 0, ∅. iFrame.
       by rewrite big_sepS_empty. }
-    iApply (refines_exists (ngR γ)).
+    iApply (refines_pack (ngR γ)).
     do 2 rel_pure_r.
     iApply refines_pair.
     - (* New name *)
diff --git a/theories/examples/stack/refinement.v b/theories/examples/stack/refinement.v
index c810915e5156f0340d652b34b10d305cc699cf04..c2984a5c04136116022c9296bcafd4d93a38309a 100644
--- a/theories/examples/stack/refinement.v
+++ b/theories/examples/stack/refinement.v
@@ -169,7 +169,7 @@ Section proof.
   Proof.
     unfold CG_stack, FG_stack.
     iApply refines_forall. iIntros (A). iAlways.
-    iApply (refines_exists (stackInt A)).
+    iApply (refines_pack (stackInt A)).
     repeat iApply refines_pair.
     - unfold CG_new_stack, FG_new_stack.
       iApply refines_arrow_val. iAlways.
diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v
index d5eace027c040e109ef03d9945d6eeed07f11af7..3a534e2c235af3ea291ce48dd64eb9c2d75a4345 100644
--- a/theories/examples/symbol.v
+++ b/theories/examples/symbol.v
@@ -235,7 +235,7 @@ Section proof.
     rel_apply_l (refines_newlock_l N (lok_inv size1 size2 tbl1 tbl2 l2)%I with "[Hs1' Hs2' Htbl1' Htbl2' Hl2]").
     { iExists 0,_. by iFrame. }
     iNext. iIntros (l1 γl) "#Hl1". rel_pure_l. rel_pure_l.
-    iApply (refines_exists (tableR γ)).
+    iApply (refines_pack (tableR γ)).
     repeat iApply refines_pair.
     (* Eq *)
     - iApply eqKey_refinement.
@@ -314,7 +314,7 @@ Section proof.
     rel_apply_l (refines_newlock_l N (lok_inv size1 size2 tbl1 tbl2 l2)%I with "[Hs1' Hs2' Htbl1' Htbl2' Hl2]").
     { iExists 0,_. by iFrame. }
     iNext. iIntros (l1 γl) "#Hl1". rel_pure_l. rel_pure_l.
-    iApply (refines_exists (tableR γ)).
+    iApply (refines_pack (tableR γ)).
     repeat iApply refines_pair.
     (* Eq *)
     - iApply eqKey_refinement.
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index d3eef81fbdd517db245e7c4bbbd64332e1700428..4d82bdc4b0f6523b8f26e97b46d16901f286fe26 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -346,7 +346,7 @@ Section refinement.
         (reloc.lib.lock.newlock, reloc.lib.lock.acquire, reloc.lib.lock.release)
     : lrel_lock.
   Proof.
-    simpl. iApply (refines_exists lockInt).
+    simpl. iApply (refines_pack lockInt).
     repeat iApply refines_pair.
     - by iApply newlock_refinement.
     - by iApply acquire_refinement_direct.
diff --git a/theories/experimental/hocap/ticket_lock.v b/theories/experimental/hocap/ticket_lock.v
index 2aa85b9594a3dbca75cd1897286f895ba0a644c2..d0f33f98240358c25cd8e7128e1c4c5fb2f972e8 100644
--- a/theories/experimental/hocap/ticket_lock.v
+++ b/theories/experimental/hocap/ticket_lock.v
@@ -126,7 +126,7 @@ Section refinement.
             <<
            (spin_lock.newlock, spin_lock.acquire, spin_lock.release) : interp lockT Δ.
   Proof.
-    iApply (refines_exists lockInt).
+    iApply (refines_pack lockInt).
     repeat iApply refines_pair; simpl.
     - by iApply newlock_refinement.
     - by iApply acquire_refinement.
diff --git a/theories/logic/compatibility.v b/theories/logic/compatibility.v
index 73c57a5c86e3a4849cf6a3638bd08bfda264e25e..2cb61fb44de178a0582e657f130208acd7837d7a 100644
--- a/theories/logic/compatibility.v
+++ b/theories/logic/compatibility.v
@@ -68,7 +68,7 @@ Section compatibility.
     - iExists #(); eauto.
   Qed.
 
-  Lemma refines_exists (A : lrel Σ) e e' (C : lrel Σ → lrel Σ) :
+  Lemma refines_pack (A : lrel Σ) e e' (C : lrel Σ → lrel Σ) :
     (REL e << e' : C A) -∗
     REL e << e' : ∃ A, C A.
   Proof.