∀ {α : Type u_7} [inst : SizeOf α] (MeasurableSet' : Set α → Prop) (measurableSet_empty : MeasurableSet' ∅)
  (measurableSet_compl : ∀ (s : Set α), MeasurableSet' s → MeasurableSet' sᶜ)
  (measurableSet_iUnion : ∀ (f : ℕ → Set α), (∀ (i : ℕ), MeasurableSet' (f i)) → MeasurableSet' (⋃ i, f i)),
  sizeOf
      { MeasurableSet' := MeasurableSet', measurableSet_empty := measurableSet_empty,
        measurableSet_compl := measurableSet_compl, measurableSet_iUnion := measurableSet_iUnion } =
    1 + sizeOf measurableSet_empty