{α : Type ua} →
  {β : Type ub} →
    [inst : UniformSpace α] →
      [inst_1 : UniformSpace β] →
        {f : α → β} →
          {motive : IsUniformEmbedding f → Sort u} →
            (t : IsUniformEmbedding f) →
              ((toIsUniformInducing : IsUniformInducing f) → (injective : Function.Injective f) → motive ⋯) → motive t