∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (C : Set (Set α)),
  m0 = MeasurableSpace.generateFrom C →
    IsPiSystem C → ∀ [MeasureTheory.IsFiniteMeasure μ], (∀ s ∈ C, μ s = ν s) → μ Set.univ = ν Set.univ → μ = ν