Det muller accept omega limit

theorem det_muller_accept_omega_limit (M : DA A) [Finite M.State] (acc : Set M.State) :    ∃ accSet, {as | M.MullerAccept accSet as} = (M.toNA.AcceptedLang acc)↗ω := by  use {acc' | (acc' ∩ acc).Nonempty} ; ext as  simp [← da_acc_omega_lang, DA.MullerAccept] ; constructor  · rintro ⟨s, h_inf, h_acc⟩    use (M.DetRun as) ; constructor    · exact da_inf_run_exists as    obtain ⟨φ, h_mono, h_s⟩ := frequently_iff_strict_mono.mp h_inf    apply frequently_iff_strict_mono.mpr    use φ ; simp [*]  · rintro ⟨ss, h_run, h_acc⟩    obtain ⟨rfl⟩ := da_inf_run_unique h_run    have : Finite M.toNA.State := by assumption    obtain ⟨s, h_s, h_inf⟩ := frequently_in_finite_set.mp h_acc    use s ; aesop