∀ {M : Type v} {α : Type w} {m : MeasurableSpace α} [inst : VAdd M α] [MeasurableConstVAdd M α] (c : M)
  (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure M α μ],
  MeasureTheory.MeasurePreserving (fun x => c +ᵥ x) μ μ = True