{α : Sort u_1} →
  {le : α → α → Bool} →
    {motive : Batteries.TotalBLE le → Sort u} →
      (t : Batteries.TotalBLE le) → ((total : ∀ {a b : α}, le a b = true ∨ le b a = true) → motive ⋯) → motive t