Buchi Family cover

theorem buchiFamily_cover [Inhabited Symbol] [Finite State] :    ⨆ i, na.buchiFamily i = ⊤ := by  apply mem_ext  intro xs  have : Finite (Quotient na.BuchiCongruence.eq) := buchiCongruence_fin_index  let color (t : Finset ℕ) : Quotient na.BuchiCongruence.eq :=    if h : t.Nonempty then ⟦ xs.extract (t.min' h) (t.max' h) ⟧ else ⟦ [] ⟧  obtain ⟨b, ns, h_ns, h_color⟩ := infinite_graph_ramsey color  obtain ⟨f, h_mono, rfl⟩ := strictMono_of_infinite h_ns  simp only [ωLanguage.mem_iSup, Prod.exists, ωLanguage.mem_top, iff_true]  use ⟦ xs.take (f 0) ⟧, b  apply mem_buchiFamily.mpr  use xs.take (f 0), xs.drop (f 0) |>.toSegs (f · - f 0)