Da acc omega lang

theorem da_acc_omega_lang :    M.toNA.AcceptedOmegaLang acc = (M.toNA.AcceptedLang acc)↗ω := by  ext as ; constructor  · rintro ⟨ss, h_run, h_inf⟩    obtain ⟨φ, h_mono, h_acc⟩ := frequently_iff_strict_mono.mp h_inf    apply frequently_iff_strict_mono.mpr    use φ ; simp [h_mono] ; intro m    use (φ m), as ; constructor <;> [skip ; rfl]    use ss ; simp [h_acc]    exact na_InfRun_iff_FinRun.mp h_run (φ m)  · simp only [instOmegaLimit, OmegaLimit, frequently_iff_strict_mono, mem_setOf_eq]    rintro ⟨φ, h_mono, h_acc⟩    use (M.DetRun as) ; constructor    · apply da_inf_run_exists    apply frequently_iff_strict_mono.mpr    use φ ; simp [h_mono] ; intro m    obtain ⟨n, as', ⟨ss, h_run', h_acc'⟩, h_as'⟩ := h_acc m    have h_as' := extract_eq_extract h_as' ; simp at h_as'    obtain ⟨rfl, h_as'⟩ := h_as'    have h_run : M.toNA.FinRun (φ m) as ss := na_FinRun_modulo      (M := M.toNA) (n := φ m) (as := as') (as' := as) (ss := ss) (ss' := ss) (by grind) (by grind) h_run'    have := da_fin_run_unique h_run (φ m) (by omega)    simp_all