∀ {α : Type u_1} [inst : Preorder α]
  (motive :
    (x : Ordnode α) →
      (x_1 : WithBot α) →
        (x_2 : WithTop α) →
          (x_3 : α) → x.Bounded x_1 x_2 → Ordnode.nil.Bounded (↑x_3) x_2 → Ordnode.All (fun x => x > x_3) x → Prop)
  (x : Ordnode α) (x_1 : WithBot α) (x_2 : WithTop α) (x_3 : α) (x_4 : x.Bounded x_1 x_2)
  (x_5 : Ordnode.nil.Bounded (↑x_3) x_2) (x_6 : Ordnode.All (fun x => x > x_3) x),
  (∀ (x : WithBot α) (x_7 : WithTop α) (x_8 : α) (x_9 : Ordnode.nil.Bounded x x_7) (hn : Ordnode.nil.Bounded (↑x_8) x_7)
      (x_10 : Ordnode.All (fun x => x > x_8) Ordnode.nil), motive Ordnode.nil x x_7 x_8 x_9 hn x_10) →
    (∀ (size : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α) (x_7 : WithBot α) (x_8 : WithTop α) (x_9 : α)
        (h₁ : l.Bounded x_7 ↑x) (h₂ : r.Bounded (↑x) x_8) (x_10 : Ordnode.nil.Bounded (↑x_9) x_8)
        (al₁ : Ordnode.All (fun x => x > x_9) l) (al₂ : x > x_9) (right : Ordnode.All (fun x => x > x_9) r),
        motive (Ordnode.node size l x r) x_7 x_8 x_9 ⋯ x_10 ⋯) →
      motive x x_1 x_2 x_3 x_4 x_5 x_6