∀ {α : Type u_2} (measureOf : Set α → ENNReal) (empty : measureOf ∅ = 0)
  (mono : ∀ {s₁ s₂ : Set α}, s₁ ⊆ s₂ → measureOf s₁ ≤ measureOf s₂)
  (iUnion_nat :
    ∀ (s : ℕ → Set α), Pairwise (Function.onFun Disjoint s) → measureOf (⋃ i, s i) ≤ ∑' (i : ℕ), measureOf (s i))
  (measureOf_1 : Set α → ENNReal) (empty_1 : measureOf_1 ∅ = 0)
  (mono_1 : ∀ {s₁ s₂ : Set α}, s₁ ⊆ s₂ → measureOf_1 s₁ ≤ measureOf_1 s₂)
  (iUnion_nat_1 :
    ∀ (s : ℕ → Set α), Pairwise (Function.onFun Disjoint s) → measureOf_1 (⋃ i, s i) ≤ ∑' (i : ℕ), measureOf_1 (s i)),
  ({ measureOf := measureOf, empty := empty, mono := mono, iUnion_nat := iUnion_nat } =
      { measureOf := measureOf_1, empty := empty_1, mono := mono_1, iUnion_nat := iUnion_nat_1 }) =
    (measureOf = measureOf_1)