Da concat of muller accept

theorem da_concat_of_muller_accept (as : Stream' A)    (h : (M1.Concat acc1 M2).MullerAccept (DA.MullerAcc_Concat M1 acc1 M2 accSet2) as) :    ∃ n, M1.toNA.FinAccept acc1 n as ∧ M2.MullerAccept accSet2 (as.drop n) := by  obtain ⟨i, h_acc2, h_some⟩ := h  obtain ⟨n, h_n⟩ := eventually_atTop.mp <| inf_occ_eventually ((M1.Concat acc1 M2).DetRun as)  have h_eventl : ∀ k ≥ n, (((M1.Concat acc1 M2).DetRun as k).2 i).isSome := by    intro k h_k ; exact h_some ((M1.Concat acc1 M2).DetRun as k) <| h_n k h_k  obtain ⟨m, h_m, h_acc1, h_suffix⟩ := da_concat_det_run_2 M1 acc1 M2 as n i h_eventl  suffices h_inf : {s2 | ∃ s ∈ InfOcc ((M1.Concat acc1 M2).DetRun as), s.2 i = some s2} = InfOcc (M2.DetRun (as.drop m)) by    use m ; constructor    · use M1.DetRun as ; simp [h_acc1]      exact da_fin_run_exists m as    · rw [h_inf] at h_acc2      exact h_acc2  ext s2 ; constructor  · rintro ⟨s, h_inf, h_s⟩    apply frequently_atTop.mpr ; intro l    obtain ⟨k, h_k, rfl⟩ := frequently_atTop.mp h_inf (m + l + 1)    simp [h_suffix k (by omega)] at h_s    use (k - m) ; simp [h_s] ; omega  · intro h_inf    obtain ⟨k, h_k, rfl⟩ := frequently_atTop.mp h_inf (n - m)    use ((M1.Concat acc1 M2).DetRun as (k + m)) ; constructor    · exact h_n (k + m) (by omega)    · simp [h_suffix (k + m) (by omega)]