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