I Own alloc strong dep

@[rocq_alias own_alloc_strong_dep]theorem iOwn_alloc_strong_dep (f : GName → F.ap (IProp GF)) (P : GName → Prop)    (HP : ∀ N, ∃ k, N ≤ k ∧ P k)    (Hf : ∀ γ, P γ → ✓ (f γ)) :    ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ iOwn γ (f γ) := by  unfold iOwn  refine .trans (Q := iprop(|==> ∃ m, ⌜∃ γ, P γ ∧ m = iSingleton F γ (f γ)⌝ ∧ UPred.ownM m)) ?_ (BIUpdate.mono ?_)  · refine .trans (@UPred.ownM_unit (IResUR GF) _ iprop(emp)) ?_    refine .trans intuitionistically_elim ?_    apply UPred.bupd_ownM_updateP    apply UpdateP.total.mpr    intros n mf Hvalid    replace Hvalid : ✓{n} mf := CMRA.validN_ne UCMRA.unit_left_id.dist Hvalid    obtain ⟨γ, Hfresh, HPγ⟩ := (mf (ElemG.τ GF F)).exists_fresh_sat HP    refine ⟨iSingleton F γ (f γ), ⟨γ, HPγ, rfl⟩, ?_⟩    apply validN_iSingleton_op Hvalid (Hf γ HPγ).validN Hfresh  · refine BI.exists_elim (fun m => BI.pure_elim_left (fun ⟨γ, HPγ, Hm⟩ => ?_))    subst Hm    exact BI.exists_intro_trans γ (BI.persistent_entails_right (BI.pure_intro HPγ))