diff --git a/iris_heap_lang/derived_laws.v b/iris_heap_lang/derived_laws.v
index 7e28862f3adb9e87b9c302e47bbc1db6bee49eab..e4e218a72904737906c412e52394756f4d73d448 100644
--- a/iris_heap_lang/derived_laws.v
+++ b/iris_heap_lang/derived_laws.v
@@ -228,7 +228,6 @@ Proof.
   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 :
    {{{ ▷ l ↦∗ vs }}} Xchg #(l +ₗ off) v @ s; E {{{ RET (vs !!! off); l ↦∗ vinsert off v vs }}}.
 Proof.
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 649c64383ab20ce935b7cb895e45af269d68c02a..87adf2a6b1a1d6aa7c4207e46c95fce3d18b4b59 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -323,7 +323,6 @@ Proof.
   iMod (gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit; first done. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
-
 Lemma wp_xchg s E l v' v :
   {{{ ▷ l ↦ v' }}} Xchg (Val $ LitV (LitLoc l)) (Val v) @ s; E
   {{{ RET v'; l ↦ v }}}.