{α : Type u_1} →
  {G : Type u_2} →
    [inst : AddCommMonoid G] →
      {C : Set (Set α)} →
        (toFun : Set α → G) →
          toFun ∅ = 0 →
            (∀ (I : Finset (Set α)), ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → toFun (⋃₀ ↑I) = ∑ u ∈ I, toFun u) →
              MeasureTheory.AddContent G C