Gen Heap init names

@[rocq_alias gen_heap_init_names]theorem genHeap_init_names [DecidableEq L] [genHeapPreS L V GF H] (σ : H V) :    ⊢ |==> ∃ γh γm : GName,      genHeapInterp (G := (⟨γh, γm⟩ : genHeapGS L V GF H)) σ ∗      ([∗map] l ↦ v ∈ σ,        pointsTo (G := (⟨γh, γm⟩ : genHeapGS L V GF H)) l (.own 1) v) ∗      ([∗map] l ↦ _v ∈ σ,        metaToken (G := (⟨γh, γm⟩ : genHeapGS L V GF H)) l ⊤) := by  imod (ghost_map_alloc_empty (K := L) (V := V)) with ⟨%γh, Hh⟩  imod (ghost_map_alloc_empty (K := L) (V := GName)) with ⟨%γm, Hm⟩  letI G : genHeapGS L V GF H := ⟨γh, γm⟩  ihave Hinterp0 : genHeapInterp (G := G) ∅ $$ [Hh Hm]  · unfold genHeapInterp    iexists (∅ : H GName)    isplitr    · ipureintro      intro k hk      simp [dom, LawfulPartialMap.get?_empty] at hk    iframe Hh Hm  imod genHeap_alloc_big σ ∅ (LawfulPartialMap.disjoint_empty_right _) $$ Hinterp0    with ⟨Hinterp, Hpts, Htok⟩  imodintro  iexists γh, γm  iframe Hpts Htok  iapply genHeapInterp_eqv (equiv_iff_eq.mpr LawfulPartialMap.union_empty_right) $$ Hinterp