Inter freq comp acc freq acc

lemma inter_freq_comp_acc_freq_acc {xs : ωSequence Symbol} {ss : ωSequence ((Π i, State i) × Bool)}    (h_run : (interNA na acc).Run xs ss)    (h_inf_f : ∃ᶠ k in atTop, ss k ∈ {s | s.fst false ∈ acc false})    (h_inf_t : ∃ᶠ k in atTop, ss k ∈ {s | s.fst true ∈ acc true}) :    ∃ᶠ k in atTop, ss k ∈ interAccept acc := by  have (k : ℕ) := (h_run.trans k).right  have h_univ : ∃ᶠ k in atTop, ss k ∈ univ := by simp [atTop_neBot]  have (b : Bool) : interAcc b acc = {⟨_, b'⟩ | b' = b} ∩ {⟨p,_⟩ | p b ∈ acc b} := by    ext; grind  have : {⟨_, b⟩ : (Π i, State i) × Bool | b = false}ᶜ = {⟨_, b⟩ | b = true} := by    ext; grind  apply frequently_leadsTo_frequently h_univ  apply leadsTo_cases_or (q := {⟨_, b⟩ | b = false}) <;>  grind [until_frequently_leadsTo_and, univ_inter]