{F : Sort u_1} →
  {α : Sort u_2} →
    {β : Sort u_3} →
      [inst : FunLike F α β] →
        {motive : EmbeddingLike F α β → Sort u} →
          (t : EmbeddingLike F α β) → ((injective' : ∀ (f : F), Function.Injective ⇑f) → motive ⋯) → motive t