Flatten fair Segs

theorem flatten_fairSegs {ps : Set P}    {ts : ωSequence (State P M S)} {xls : ωSequence (List (Action P M))}    (hmtr : ∀ k, a.lts.MTr (ts k) (xls k) (ts (k + 1)))    (hpos : ∀ k, (xls k).length > 0)    (hsch : ∀ k m, m ∈ (ts k).msgs → m.dest ∈ ps → some m ∈ xls k) :    ∃ ss, a.lts.OmegaExecution ss xls.flatten ∧ (∀ k, ss (xls.cumLen k) = ts k) ∧      ∀ p, p ∈ ps → ProcFair p ss xls.flatten := by  obtain ⟨ss, h_omega, h_ts⟩ := LTS.OmegaExecution.flatten_mTr hmtr hpos  use ss, h_omega, h_ts  rintro p h_m m ⟨rfl⟩  by_contra! ⟨k, h_k, h_k'⟩  have h_xls : ∃ᶠ n in atTop, n ∈ xls.cumLen '' univ := by    apply frequently_iff_strictMono.mpr    use xls.cumLen    grind [cumLen_strictMono]  obtain ⟨j, _, h_j⟩ : ∃ j, k ≤ xls.cumLen j ∧ m ∈ (ts j).msgs := by    obtain ⟨n, _, j, _, _⟩ := frequently_atTop.mp h_xls k    grind [Algorithm.omega_notRcvd_enabled h_omega h_k h_k']  obtain ⟨i, _, _⟩ := List.getElem_of_mem <| hsch j m h_j h_m  grind [extract_flatten hpos j]