State init Heap self

theorem State.initHeap_self {σ : State} {l : Loc} {v : Option Val}    (h : PartialMap.get? (M := HeapF) σ.heap l = some v) : σ.initHeap l 1 v = σ := by  have hl : l + (0 : Int) = l := by    cases l    simp only [HAdd.hAdd, Loc.mk.injEq]    grind  have hins : Std.insert (M := HeapF) σ.heap l v = σ.heap := by    refine Std.LawfulPartialMap.equiv_iff_eq.mp fun k => ?_    rw [Std.LawfulPartialMap.get?_insert]    split    · next heq => exact heq ▸ h.symm    · rfl  simp only [State.initHeap, Int.toNat_one, List.range_one, List.foldl_cons, List.foldl_nil,    Int.cast_ofNat_Int, hl, hins]