Fupd mask frame acc

@[rocq_alias fupd_mask_frame_acc]theorem fupd_mask_frame_acc {E E' E1 E2 : CoPset} {P Q : PROP}:    E1 ⊆ E → (|={E1,E1 \ E2}=> Q) ⊢    (Q -∗ |={E \ E2,E'}=> (∀ R, (|={E1 \ E2,E1}=> R) -∗ |={E \ E2,E}=> R) -∗  P) -∗    (|={E,E'}=> P) := λ hE => by  have hmask : E \ E2 ⊆ (E1 \ E2) ∪ (E \ E1) := by    intro x hx; rw [mem_diff] at hx    by_cases hx1 : x ∈ E1    · exact mem_union.2 <| .inl <| mem_diff.2 ⟨hx1, hx.2⟩    · exact mem_union.2 <| .inr <| mem_diff.2 ⟨hx.1, hx1⟩  have hdisj : (E1 \ E2) ## (E \ E1) := disjoint_subset_left diff_subset_left disjoint_diff_right  refine wand_intro <| frame_right.trans <| (BIFUpdate.mono wand_elim_right).trans ?_  refine (BIFUpdate.mono ?_).trans <| fupd_mask_frame hE  refine sep_emp.2.trans <| (sep_mono_right <| fupd_mask_intro_subseteq hmask).trans ?_  refine fupd_frame_left.trans <| (BIFUpdate.mono frame_right).trans <| fupd_elim ?_  refine BIFUpdate.mono <| sep_symm.trans ?_  refine (sep_mono ?_ .rfl).trans wand_elim_right  refine forall_intro λ R => wand_intro <| frame_right.trans <| fupd_elim ?_  exact emp_sep.1.trans <| (fupd_mask_frame_right hdisj).trans <| by simp [subset_union_diff hE]