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