Ghost map alloc strong

@[rocq_alias ghost_map_alloc_strong]theorem ghost_map_alloc_strong [DecidableEq K] (P : GName → Prop) (m : H V) :  (∀ N, ∃ k, N ≤ k ∧ P k) →  ⊢@{IProp GF} |==> ∃ γ, ⌜P γ⌝ ∗ (γ ↪●MAP m) ∗ [∗map] k ↦ v ∈ m, γ ↪◯MAP[k] v := by  unfold ghost_map_elem ghost_map_auth  iintro %Hinf  imod iOwn_alloc_strong (E := GhostMapG.elem)    (Auth (DFrac.own 1) (V := Agree (DiscreteO V)) (∅ : H _)) P Hinf with ⟨%γ, %HP, G⟩  · simpa only [auth_valid_iff] using DFrac.valid_own_one  · iexists γ; iframe %HP    iapply BIUpdate.mono <| sep_mono_right <| bigOpM_iOwn_entail γ _ m    iapply BIUpdate.mono <| iOwn_op.mp    iapply iOwn_update $$ G    refine Update.equiv_right ?_      (update_big_alloc _ (Std.PartialMap.map (fun x ↦ toAgree ⟨x⟩) m) _        (disjoint_empty_right _) DFrac.valid_own_one        (all_map fun _ _ => Agree.toAgree_valid))    refine CMRA.op_eqv ?_ (BigOpM.bigOpM_map_eqv _ _ _)    exact OFE.NonExpansive.eqv (OFE.Equiv.of_eq union_empty_right)