∀ {α : Sort u} {b : α} {motive : (x y : Lean.Order.FlatOrder b) → x.rel y → Prop} {x y : Lean.Order.FlatOrder b}
  (t : x.rel y),
  (∀ {x : Lean.Order.FlatOrder b}, motive b x ⋯) → (∀ {x : Lean.Order.FlatOrder b}, motive x x ⋯) → motive x y t