{α : Type u} →
  {β : Type v} →
    {γ : Type w} →
      {motive : HShiftLeft α β γ → Sort u_1} →
        (t : HShiftLeft α β γ) → ((hShiftLeft : α → β → γ) → motive { hShiftLeft := hShiftLeft }) → motive t