∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P P_1 : Finpartition Finset.univ} (e_P : P = P_1)
  (hP : P.IsEquipartition) (G G_1 : SimpleGraph α),
  G = G_1 →
    ∀ {inst_2 : DecidableRel G.Adj} [inst_3 : DecidableRel G_1.Adj] (ε ε_1 : ℝ),
      ε = ε_1 → SzemerediRegularity.increment hP G ε = SzemerediRegularity.increment ⋯ G_1 ε_1