diff --git a/iris_heap_lang/derived_laws.v b/iris_heap_lang/derived_laws.v
index d4a33a5685a2460977dbda9c0c28b57c2a5733cc..a6029e8719d1d365a79185c1f349f34bbe301e3b 100644
--- a/iris_heap_lang/derived_laws.v
+++ b/iris_heap_lang/derived_laws.v
@@ -207,36 +207,40 @@ Qed.
 
 Lemma twp_xchg_offset s E l off vs v v' :
   vs !! off = Some v →
-  val_is_unboxed v ->
+  val_is_unboxed v →
+  val_is_unboxed v' →
   [[{ l ↦∗ vs }]] Xchg #(l +ₗ off) v' @ s; E [[{ RET v; l ↦∗ <[off:=v']> vs }]].
 Proof.
-  iIntros (Hlookup Hunboxed Φ) "Hl HΦ".
+  iIntros (Hlookup Hunboxed Hunboxed' Φ) "Hl HΦ".
   iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
   iApply (twp_xchg with "Hl1") => //. iIntros "Hl1".
   iApply "HΦ". iApply "Hl2". iApply "Hl1".
 Qed.
 Lemma wp_xchg_offset s E l off vs v v' :
-  (vs !! off) = Some v →
-  val_is_unboxed v ->
+  vs !! off = Some v →
+  val_is_unboxed v →
+  val_is_unboxed v' →
   {{{ ▷ l ↦∗ vs }}} Xchg #(l +ₗ off) v' @ s; E {{{ RET v; l ↦∗ <[off:=v']> vs }}}.
 Proof.
-  iIntros (? ? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
+  iIntros (? ? ? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
   iApply (twp_xchg_offset with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
 Qed.
 
 Lemma twp_xchg_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v :
-   val_is_unboxed (vs !!! off) ->
+   val_is_unboxed (vs !!! off) →
+   val_is_unboxed v →
   [[{ l ↦∗ vs }]] Xchg #(l +ₗ off) v @ s; E [[{ RET (vs !!! off); l ↦∗ vinsert off v vs }]].
 Proof.
-  intros ?. setoid_rewrite vec_to_list_insert. apply twp_xchg_offset => //.
+  intros ? ?. setoid_rewrite vec_to_list_insert. apply twp_xchg_offset => //.
   by apply vlookup_lookup.
 Qed.
 
 Lemma wp_xchg_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v :
-   val_is_unboxed (vs !!! off) ->
+   val_is_unboxed (vs !!! off) →
+   val_is_unboxed v →
   {{{ ▷ l ↦∗ vs }}} Xchg #(l +ₗ off) v @ s; E {{{ RET (vs !!! off); l ↦∗ vinsert off v vs }}}.
 Proof.
-  iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
+  iIntros (? ? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
   iApply (twp_xchg_offset_vec with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
 Qed.
 
diff --git a/iris_heap_lang/lang.v b/iris_heap_lang/lang.v
index 5a58f32b4229b4a7752049a8a0b67a2b0511e4d4..6a69cb3413c471f518b6e6df7942489206ea2fae 100644
--- a/iris_heap_lang/lang.v
+++ b/iris_heap_lang/lang.v
@@ -334,10 +334,10 @@ Proof.
      | Load e => GenNode 15 [go e]
      | Store e1 e2 => GenNode 16 [go e1; go e2]
      | CmpXchg e0 e1 e2 => GenNode 17 [go e0; go e1; go e2]
-     | Xchg e0 e1 => GenNode 21 [go e0; go e1]
-     | FAA e1 e2 => GenNode 18 [go e1; go e2]
-     | NewProph => GenNode 19 []
-     | Resolve e0 e1 e2 => GenNode 20 [go e0; go e1; go e2]
+     | Xchg e0 e1 => GenNode 18 [go e0; go e1]
+     | FAA e1 e2 => GenNode 19 [go e1; go e2]
+     | NewProph => GenNode 20 []
+     | Resolve e0 e1 e2 => GenNode 21 [go e0; go e1; go e2]
      end
    with gov v :=
      match v with
@@ -371,10 +371,10 @@ Proof.
      | GenNode 15 [e] => Load (go e)
      | GenNode 16 [e1; e2] => Store (go e1) (go e2)
      | GenNode 17 [e0; e1; e2] => CmpXchg (go e0) (go e1) (go e2)
-     | GenNode 18 [e1; e2] => FAA (go e1) (go e2)
-     | GenNode 19 [] => NewProph
-     | GenNode 20 [e0; e1; e2] => Resolve (go e0) (go e1) (go e2)
-     | GenNode 21 [e0; e1] => Xchg (go e0) (go e1)
+     | GenNode 18 [e0; e1] => Xchg (go e0) (go e1)
+     | GenNode 19 [e1; e2] => FAA (go e1) (go e2)
+     | GenNode 20 [] => NewProph
+     | GenNode 21 [e0; e1; e2] => Resolve (go e0) (go e1) (go e2)
      | _ => Val $ LitV LitUnit (* dummy *)
      end
    with gov v :=
@@ -685,6 +685,7 @@ Inductive head_step : expr → state → list observation → expr → state →
   | XchgS l v1 v2 σ :
      σ.(heap) !! l = Some $ Some v1 →
      val_is_unboxed v1 →
+     val_is_unboxed v2 →
      head_step (Xchg (Val $ LitV $ LitLoc l) (Val v2)) σ
                []
                (Val v1) (state_upd_heap <[l:=Some v2]> σ)
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index eb0cd29af72c871d9e1ad3089c4a6241eb531595..dffccaa399d8169c468d1c5390b54b44e38a0fb8 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -313,11 +313,12 @@ Proof.
 Qed.
 
 Lemma twp_xchg s E l v' v :
-  val_is_unboxed v' ->
+  val_is_unboxed v →
+  val_is_unboxed v' →
   [[{ l ↦ v' }]] Xchg (Val $ LitV $ LitLoc l) (Val v) @ s; E
   [[{ RET v'; l ↦ v }]].
 Proof.
-  iIntros (? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
+  iIntros (Hv Hv' Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
   iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto with head_step.
   iIntros (κ v2 σ2 efs Hstep); inv_head_step.
@@ -326,11 +327,12 @@ Proof.
 Qed.
 
 Lemma wp_xchg s E l v' v :
-  val_is_unboxed v' ->
+  val_is_unboxed v →
+  val_is_unboxed v' →
   {{{ ▷ l ↦ v' }}} Xchg (Val $ LitV (LitLoc l)) (Val v) @ s; E
   {{{ RET v'; l ↦ v }}}.
 Proof.
-  iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
+  iIntros (Hv Hv' Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
   iApply (twp_xchg with "H"); [by auto..|]. iIntros "H HΦ". by iApply "HΦ".
 Qed.
 
diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index fa98c676267f0bf48cdfb7da17c8c7e57d67886b..ab18be35d326efad2999511b6bc0ec4b91492e34 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -373,14 +373,15 @@ Qed.
 Lemma tac_wp_xchg Δ Δ' s E i K l v v' Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
-  val_is_unboxed v ->
+  val_is_unboxed v' →
+  val_is_unboxed v  →
   match envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' with
   | Some Δ'' => envs_entails Δ'' (WP fill K (Val $ v) @ s; E {{ Φ }})
   | None => False
   end →
   envs_entails Δ (WP fill K (Xchg (LitV l) (Val v')) @ s; E {{ Φ }}).
 Proof.
-  rewrite envs_entails_eq=> ????.
+  rewrite envs_entails_eq=> ?????.
   destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
   rewrite -wp_bind. eapply wand_apply; first by eapply wp_xchg.
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
@@ -389,7 +390,8 @@ Proof.
 Qed.
 Lemma tac_twp_xchg Δ s E i K l v v' Φ :
   envs_lookup i Δ = Some (false, l ↦ v)%I →
-  val_is_unboxed v ->
+  val_is_unboxed v' →
+  val_is_unboxed v →
   match envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ with
   | Some Δ' => envs_entails Δ' (WP fill K (Val $ v) @ s; E [{ Φ }])
   | None => False
diff --git a/iris_heap_lang/proph_erasure.v b/iris_heap_lang/proph_erasure.v
index 202b61c4a2191335df99d4d7a4f46399a4e28866..8ea48fb209593db102a107de9578f31b019da8de 100644
--- a/iris_heap_lang/proph_erasure.v
+++ b/iris_heap_lang/proph_erasure.v
@@ -279,17 +279,18 @@ Proof.
   eexists _, _, _, _; simpl; split; first econstructor; eauto.
 Qed.
 Lemma erased_head_step_head_step_Xchg l v w σ :
-  val_is_unboxed v ->
+  val_is_unboxed v →
+  val_is_unboxed w →
   erase_heap (heap σ) !! l = Some (Some v) →
   head_steps_to_erasure_of (Xchg #l w) σ v
    {| heap := <[l:=Some $ erase_val w]> (erase_heap (heap σ)); used_proph_id := ∅ |} [].
 Proof.
-  intros ? Hl.
+  intros Hv Hw Hl.
   rewrite lookup_erase_heap in Hl.
   destruct (heap σ !! l) as [[|]|] eqn:?; simplify_eq/=.
+  rewrite val_is_unboxed_erased in Hv * => //; intros Hv.
   eexists _, _, _, _; simpl; split; first econstructor; repeat split; eauto.
-  - rewrite val_is_unboxed_erased in H * => //.
-  - rewrite /state_upd_heap /erase_state /= erase_heap_insert_Some //.
+  rewrite /state_upd_heap /erase_state /= erase_heap_insert_Some //.
 Qed.
 Lemma erased_head_step_head_step_Store l v w σ :
   erase_heap (heap σ) !! l = Some (Some v) →
@@ -358,6 +359,8 @@ Proof.
              apply un_op_eval_erase in H as [? [? ?]]
            | H : bin_op_eval _ (erase_val _) (erase_val _) = Some _ |- _ =>
              apply bin_op_eval_erase in H as [? [? ?]]
+           | H : val_is_unboxed (erase_val _) |- _ =>
+             apply -> val_is_unboxed_erased in H
            end; simplify_eq/=;
     try (by repeat econstructor);
   eauto using erased_head_step_head_step_rec,
@@ -722,13 +725,14 @@ Proof.
 Qed.
 
 Lemma head_step_erased_prim_step_xchg σ l v w :
-  val_is_unboxed v ->
+  val_is_unboxed v →
+  val_is_unboxed w →
   heap σ !! l = Some (Some v) →
   ∃ e2' σ2' ef', prim_step (Xchg #l (erase_val w)) (erase_state σ) [] e2' σ2' ef'.
 Proof.
-  intros ? Hw. do 3 eexists; apply head_prim_step; econstructor.
-  - rewrite /erase_state /state_upd_heap /= lookup_erase_heap Hw; eauto.
-  - by rewrite val_is_unboxed_erased.
+  intros Hv Hw Hl. do 3 eexists; apply head_prim_step; econstructor.
+  1: rewrite /erase_state /state_upd_heap /= lookup_erase_heap Hl; eauto.
+  1,2: by rewrite val_is_unboxed_erased.
 Qed.
 
 Lemma head_step_erased_prim_step_store σ l v w :