∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {S T : Set (Set α)},
  m0 = MeasurableSpace.generateFrom S →
    T.Countable →
      IsPiSystem S →
        ⋃₀ T = Set.univ → (∀ t ∈ T, μ t ≠ ⊤) → (∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)) → (∀ t ∈ T, μ t = ν t) → μ = ν