{α : Type u_1} →
  [inst : Preorder α] →
    {lo : WithBot α} →
      {t : Ordnode α} →
        {hi : WithTop α} →
          {motive : Ordnode.Valid' lo t hi → Sort u} →
            (t_1 : Ordnode.Valid' lo t hi) →
              ((ord : t.Bounded lo hi) → (sz : t.Sized) → (bal : t.Balanced) → motive ⋯) → motive t_1