{α : Sort u_1} →
  {r : α → α → Prop} →
    {motive : IsLinearOrder α r → Sort u} →
      (t : IsLinearOrder α r) →
        ([toIsPartialOrder : IsPartialOrder α r] → [toTotal : Std.Total r] → motive ⋯) → motive t