∀ {α : Type u_4} [inst : UniformSpace α] (pkg : AbstractCompletion.{u_2, u_4} α) {β : Type u_3}
  [inst_1 : UniformSpace β] (pkg' : AbstractCompletion.{u_1, u_3} β) (e : α ≃ᵤ β),
  UniformContinuous (pkg'.map pkg ⇑e.symm)