Some tweaks.

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 Φ :

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).