∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (G : SimpleGraph α) [inst_2 : DecidableRel G.Adj] {ε : ℝ}
  {l : ℕ},
  0 < ε →
    l ≤ Fintype.card α →
      ∃ P, P.IsEquipartition ∧ l ≤ P.parts.card ∧ P.parts.card ≤ SzemerediRegularity.bound ε l ∧ P.IsUniform G ε