diff --git a/theories/logic/compatibility.v b/theories/logic/compatibility.v
index 96ad668e269c688a9dd57c4ec5e541deea158367..5e14b322aaab575f512f45fb1b72a6c6224a8c32 100644
--- a/theories/logic/compatibility.v
+++ b/theories/logic/compatibility.v
@@ -108,5 +108,22 @@ Section compatibility.
     value_case.
   Qed.
 
+  Lemma refines_load e e' A :
+    (REL e << e' : ref A) -∗
+    REL !e << !e' : A.
+  Proof.
+    iIntros "H".
+    rel_bind_ap e e' "H" v v' "H".
+    iDestruct "H" as (l l' -> ->) "#H".
+    rel_load_l_atomic.
+    iInv (relocN .@ "ref" .@ (l,l')) as (w w') "[Hw1 [>Hw2 #Hw]]" "Hclose"; simpl.
+    iModIntro. iExists _; iFrame "Hw1".
+    iNext. iIntros "Hw1".
+    rel_load_r.
+    iMod ("Hclose" with "[Hw1 Hw2]").
+    { iNext. iExists w,w'; by iFrame. }
+    value_case.
+  Qed.
+
 End compatibility.
 
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index 99840fe5b9325f80f99008e755b9c53644343316..f4e79645560e1c7b9d82b3cd8665fd16f0ac6071 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -259,16 +259,8 @@ Section fundamental.
   Proof.
     iIntros "IH".
     intro_clause.
-    rel_bind_ap e e' "IH" v v' "IH".
-    iDestruct "IH" as (l l') "(% & % & Hinv)"; simplify_eq/=.
-    rel_load_l_atomic.
-    iInv (relocN .@ "ref" .@ (l,l')) as (w w') "[Hw1 [>Hw2 #Hw]]" "Hclose"; simpl.
-    iModIntro. iExists _; iFrame "Hw1".
-    iNext. iIntros "Hw1".
-    rel_load_r.
-    iMod ("Hclose" with "[Hw1 Hw2]").
-    { iNext. iExists w,w'; by iFrame. }
-    value_case.
+    iApply refines_load.
+    by iApply "IH".
   Qed.
 
   Lemma bin_log_related_store Δ Γ e1 e2 e1' e2' τ :