{motive : CpltSepUniformSpace → Sort u_1} →
  (t : CpltSepUniformSpace) →
    ((α : Type u) →
        [isUniformSpace : UniformSpace α] →
          [isCompleteSpace : CompleteSpace α] →
            [isT0 : T0Space α] →
              motive { α := α, isUniformSpace := isUniformSpace, isCompleteSpace := isCompleteSpace, isT0 := isT0 }) →
      motive t