{α : Sort u_1} →
  {cmp : α → α → Ordering} →
    {motive : Batteries.TransCmp cmp → Sort u} →
      (t : Batteries.TransCmp cmp) →
        ([toOrientedCmp : Batteries.OrientedCmp cmp] →
            (le_trans : ∀ {x y z : α}, cmp x y ≠ Ordering.gt → cmp y z ≠ Ordering.gt → cmp x z ≠ Ordering.gt) →
              motive ⋯) →
          motive t