∀ {M : Type v} {α : Type w} [inst : VAdd M α] {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}
  [MeasureTheory.VAddInvariantMeasure M α μ] [MeasureTheory.VAddInvariantMeasure M α ν],
  MeasureTheory.VAddInvariantMeasure M α (μ + ν)