{α : Type u} →
  {β : Type v} →
    {γ : Type w} →
      {motive : Std.Roi.Sliceable α β γ → Sort u_1} →
        (t : Std.Roi.Sliceable α β γ) → ((mkSlice : α → Std.Roi β → γ) → motive { mkSlice := mkSlice }) → motive t