diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index e3122bfd9108fc9e7992f53fb98737a54de28483..1185095aba944821bd3284a0598e176819841027 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -36,10 +36,8 @@ Proof.
   iIntros  "[HP HΦ]". iFrame "HP". iNext.
   iIntros {v2 σ2 ef} "[% HP]".
   (* FIXME: I should not have to refer to "H0". *)
-  destruct H0 as (l & -> & ? & -> & ?).
-  rewrite -(of_to_val (Loc l) (LocV l)) // in H0.
-  apply of_val_inj in H0 as ->.
-  simpl. iSplitL; last done. iApply "HΦ" {l}. iSplit; done.
+  destruct H0 as (l & -> & [= <-]%of_to_val_flip & -> & ?); simpl.
+  iSplit; last done. iApply "HΦ"; by iSplit.
 Qed.
 
 Lemma wp_load_pst E σ l v Φ :
diff --git a/program_logic/language.v b/program_logic/language.v
index 45834b1f836a7324e8c4df4dbac6d14661a46b02..d361644f255acfb677ebbf59bd3292ca9ebd17c1 100644
--- a/program_logic/language.v
+++ b/program_logic/language.v
@@ -46,6 +46,8 @@ Section language.
        prim_step e1 σ1 e2 σ2 ef →
        step ρ1 ρ2.
 
+  Lemma of_to_val_flip v e : of_val v = e → to_val e = Some v.
+  Proof. intros <-. by rewrite to_of_val. Qed.
   Lemma reducible_not_val e σ : reducible e σ → to_val e = None.
   Proof. intros (?&?&?&?); eauto using val_stuck. Qed.
   Lemma atomic_of_val v : ¬atomic (of_val v).