diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 9f64f3cb7bae2bba26b95edf411a07a76b2e9790..62a47dfb3b13dff9051fd407e7957fc228b2a8bd 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -143,12 +143,12 @@ Section gen_heap.
   Qed.
 
   Lemma gen_heap_alloc_gen σ σ' :
-    σ ##ₘ σ' → gen_heap_ctx σ ==∗ gen_heap_ctx (σ' ∪ σ) ∗ [∗ map] l ↦ v ∈ σ', l ↦ v.
+    σ' ##ₘ σ → gen_heap_ctx σ ==∗ gen_heap_ctx (σ' ∪ σ) ∗ [∗ map] l ↦ v ∈ σ', l ↦ v.
   Proof.
     revert σ; induction σ' as [| l v σ' Hl IHσ'] using map_ind;
       iIntros (σ Hσdisj) "Hσ".
     - by rewrite left_id big_opM_empty; iFrame.
-    - iMod (IHσ' with "Hσ") as "[Hσ m]"; first by eapply map_disjoint_insert_r.
+    - iMod (IHσ' with "Hσ") as "[Hσ m]"; first by eapply map_disjoint_insert_l.
       rewrite big_opM_insert //; iFrame.
       assert (σ !! l = None).
       { eapply map_disjoint_Some_r; first by eauto.
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 653bd26bbd4b67626f573ebe7a4051ea5a29ce6b..64c807b782efe1763a242dee7481b6e094378d63 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -512,6 +512,7 @@ Proof.
   move: Hj. rewrite Z2Nat.id // => ?. by rewrite Hdisj.
 Qed.
 
+(* [h] is added on the right here to make [state_init_heap_singleton] true. *)
 Definition state_init_heap (l : loc) (n : Z) (v : val) (σ : state) : state :=
   state_upd_heap (λ h, heap_array l (replicate (Z.to_nat n) v) ∪ h) σ.
 
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 514c533d8e3ed8451e15bfa47b2d231f7aea2097..99016dec4796c5e64a11adcca0feafc02031f3ab 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -238,8 +238,7 @@ Proof.
   iIntros (σ1 κ κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia.
   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_alloc_gen with "Hσ") as "[Hσ Hl]".
-  { symmetry.
-    apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
+  { apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
     rewrite replicate_length Z2Nat.id; auto with lia. }
   iModIntro; iSplit; auto.
   iFrame. iApply "HΦ".
@@ -254,8 +253,7 @@ Proof.
   iIntros (σ1 κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia.
   iIntros (κ v2 σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_alloc_gen with "Hσ") as "[Hσ Hl]".
-  { symmetry.
-    apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
+  { apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
     rewrite replicate_length Z2Nat.id; auto with lia. }
   iModIntro; iSplit; auto.
   iFrame; iSplit; auto. iApply "HΦ".