∀ {M : Type u_2} {α : Type u_3} [inst : VAdd M α] [inst_1 : MeasurableSpace M] [inst_2 : MeasurableSpace α]
  [toMeasurableConstVAdd : MeasurableConstVAdd M α], (∀ (x : α), Measurable fun x_1 => x_1 +ᵥ x) → MeasurableVAdd M α