Acc omega lang inter2

theorem acc_omega_lang_inter2 :    (NA.OI2 M acc).AcceptedOmegaLang (NA.OI2_Acc M acc) = ⋂ i : Fin 2, (M i).AcceptedOmegaLang (acc i) := by  ext as ; simp [NA.AcceptedOmegaLang, NA.BuchiAccept]  constructor  · rintro ⟨ss, h_run, h_inf⟩ i    have h_run1 := na_hist_inf_run_proj h_run    have h_run' := na_prod_inf_run.mp h_run1 i    use (fun k ↦ (Prod.fst ∘ ss) k i) ; constructor    · assumption    let p0 k := ss k ∈ { s | s.1 0 ∈ acc 0 ∧ s.2 = 0 }    let p1 k := ss k ∈ { s | s.1 1 ∈ acc 1 ∧ s.2 = 1 }    have h_inf_or : ∃ᶠ k in atTop, p0 k ∨ p1 k := by exact h_inf    rw [frequently_or_distrib] at h_inf_or    let p0' k := (Prod.fst ∘ ss) k 0 ∈ acc 0    let p1' k := (Prod.fst ∘ ss) k 1 ∈ acc 1    have h_p0_p0' : ∀ k, p0 k → p0' k := by intro k ; simp [p0, p0'] ; tauto    have h_p1_p1' : ∀ k, p1 k → p1' k := by intro k ; simp [p1, p1'] ; tauto    revert i ; rw [Fin.forall_fin_two]    constructor <;> intro h_run_i    · rcases h_inf_or with h_inf0 | h_inf1      · exact Frequently.mono h_inf0 h_p0_p0'      · rw [← na_oi2_lemma1 M acc h_run] at h_inf1        exact Frequently.mono h_inf1 h_p0_p0'    · rcases h_inf_or with h_inf0 | h_inf1      · rw [na_oi2_lemma1 M acc h_run] at h_inf0        exact Frequently.mono h_inf0 h_p1_p1'      · exact Frequently.mono h_inf1 h_p1_p1'  · intro h_all    choose ss h_ss using h_all    let ss' := fun k i ↦ ss i k    have h_ss' : ∀ i, (M i).InfRun as (fun k ↦ ss' k i) := by intro i ; exact (h_ss i).1    have h_run' := na_prod_inf_run.mpr h_ss'    have h_hist_init : NA.OI2_HistInit.Nonempty := by simp [NA.OI2_HistInit]    have h_hist_next : ∀ s a, (NA.OI2_HistNext M acc s a).Nonempty := by      intro s a ; simp only [NA.OI2_HistNext]      rcases Classical.em (s.1 0 ∈ acc 0 ∧ s.2 = 0) with cond1 | cond1 <;> simp [cond1]      rcases Classical.em (s.1 1 ∈ acc 1 ∧ s.2 = 1) with cond2 | cond2 <;> simp [cond2]    have h_runh := na_hist_inf_run_exists h_hist_init h_hist_next h_run'    obtain ⟨hs, h_run⟩ := h_runh    use (fun k ↦ (ss' k, hs k))    constructor    · assumption    have h_inf0 : ∃ᶠ k in atTop, ss' k ∈ { s | s 0 ∈ acc 0 } := by simp [ss', (h_ss 0).2]    have h_inf1 : ∃ᶠ k in atTop, ss' k ∈ { s | s 1 ∈ acc 1 } := by simp [ss', (h_ss 1).2]    exact na_oi2_lemma2 M acc h_run h_inf0 h_inf1