∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α)
  (μ : MeasureTheory.VectorMeasure α ENNReal),
  MeasureTheory.VectorMeasure.MutuallySingular s μ ↔ s.totalVariation.MutuallySingular μ.ennrealToMeasure