∀ {α : Type u_1} (motive : Ordnode α → Sort u_2) (size : ℕ) (l : Ordnode α) (x : α) (h_1 : Unit → motive Ordnode.nil)
  (h_2 : (size : ℕ) → (l : Ordnode α) → (x : α) → motive (Ordnode.node size l x Ordnode.nil))
  (h_3 :
    (size : ℕ) →
      (l : Ordnode α) →
        (x : α) →
          (sz : ℕ) →
            (l' : Ordnode α) → (y : α) → (r' : Ordnode α) → motive (Ordnode.node size l x (Ordnode.node sz l' y r'))),
  (match Ordnode.node size l x Ordnode.nil with
    | Ordnode.nil => h_1 ()
    | Ordnode.node size l x Ordnode.nil => h_2 size l x
    | Ordnode.node size l x (Ordnode.node sz l' y r') => h_3 size l x sz l' y r') =
    h_2 size l x