Sort u →
  {α : Type u_5} →
    {β : Type u_6} →
      {γ : Type u_7} →
        Function.HasUncurry α β γ →
          {α' : Type u_5} → {β' : Type u_6} → {γ' : Type u_7} → Function.HasUncurry α' β' γ' → Sort u