∀ (M : Type v) (N : Type w) (X : Type x) [inst : UniformSpace X] [inst_1 : VAdd M X] [inst_2 : VAdd N X]
  [VAddCommClass M N X] [UniformContinuousConstVAdd M X] [UniformContinuousConstVAdd N X],
  VAddCommClass M N (UniformSpace.Completion X)